| Age | Commit message (Collapse) | Author |
|---|
|
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.
Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.
(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
This required improving the machinery of the test-suite Makefile to
support -compile.
|
