I have just upgraded my operating system, which has also involved
getting Coq 8.12.2 (December 2020)
Previously I was using Coq 8.11.2
The command
Add LoadPath "../tense-lns".
now seems to cause an error.
How do I change the command to get the same behaviour?
BTW, I've had a great deal of advice on the Coq-Club mailing list
about using a _CoqProject file, but it seems I can't do this without
stuffing up everyone who uses the same code - at any rate, early last
year, for several days, and over a dozen emails to the list, and lots
of advice from people then too, I tried to use a _CoqProject file
but it seemed either not possible or so difficult that it was
effectively impossible.
At any rate, my question now is about importing a compiled file,
say ../tense-lns/genT.vo, which (to quote an error message)
"contains library genT and not library xx.genT"
My code worked great using the Add LoadPath command above,
in Coq 8.11.2 (and earlier). So I just am asking how to do that now
(without being stuck using Coq 8.11 for ever)
You don’t absolutely have to use a _CoqProject file or coq_makefile if it doesn’t work for you (although this is surprising). But if you want to import compiled files, you do need to associate a logical name (e.g. Foo) to a directory. You should compile these files with the -R or -Q option of coqc to do so. Then you can use the command written by Emilio above, and you can import your files with From Foo Require Import ... (the From Foo is optional if you used the -R option).
Surely it is a good thing that a Coq source file should be usable by
multiple people (who may be using different versions of Coq), or that a
user should be able to switch to a more recent version without having
all his source files break.
I realize that with some generally beneficial changes this may be
unavoidable, but I find it hard to imagine why that should be so in this
case.
The justification that was given was to simplify the code managing the loadpaths. See the PR here.
We do take great care in ensuring that all the implemented changes have a minimal impact or are sufficiently justified when they have a larger impact. We have a CI infrastructure that tests dozens of external projects and millions of lines of Coq to assess the impact of these changes. In this particular case, the tests revealed no use in these projects. I think that almost all Coq users already qualified their loadpaths before (and managed it through things like _CoqProject, which only works with qualified loadpaths anyway).
Note that when we merge breaking changes, we ensure that there are backward-compatible fixes. In this case, the Add LoadPath ... as ... command is the backward-compatible fix, as it works with previous versions of Coq as well.
Indeed the change was made because adding paths to the loadpath without a proper qualitification had very confusing semantics, in particular w.r.t. shadowing other possible modules, stability under substitution / composition etc… Additionally, most times the unqualified form of loadpath was used by people led to some problems because of the above issues.
So now every (load) path has to be associated to a logical name, using Add LoadPath dir as name, which is an easy and backwards compatible change.