Why does bedrock2 use `Load`? about bedrock2 HOT 2 CLOSED

LiveVerif.v ends in the middle of a section:

This is intended, and therefore LifeVerif.v is excluded from the build. You should never try to build LifeVerif.v on its own.

LifeVerif.v contains a lot of setup code (such as setting up a Ring that depends on section variables) that I don't want to repeat in every file, and setup code that depends on section variables also can't be put into a file that other files then Import, so I use Load. The files (currently only 1) doing Load LiveVerif. are not syntactically balanced wrt Section and End: The opening of the Section LiveVerif happens through the Load, whereas the End LiveVerif is directly in the file, so I guess tools which want to parse or analyze this file and care about well-balanced Section/End need to inline Loaded files, sorry for breaking your tool Jason... 😉

from bedrock2.

sorry for breaking your tool Jason... 😉

The biggest problem is that coqc will dump locations from the loaded file into the glob file for the file doing the loading, and of course using locations from LiveVerif.v when dealing with swap.v makes no sense. The secondary problem is that my tool doesn't know how to inline Load, in large part because the .glob file contains no information about which file Coq actually picked up to inline.

from bedrock2.