| Age | Commit message (Collapse) | Author |
|---|
|
Close #14074
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
|
|
|
|
On windows we provide a way to set environment variables
local to a coq installation by providing a file
named "coq_environment.txt" containing KEY="value" pairs.
No space between KEY and = is allowed, values are in
quotes according to OCaml's escaping conventions.
The file is line-directed, illformed lines are skipped.
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
|
|
I left the other test as a v file since it might become relevant when the
corresponding Qed bug is fixed.
|
|
|
|
|
|
Closes #12351.
We set the parameters of the redirect formatter to be same than the
ones in stdout.
I guess the original semantics was to ignore the parameters, so I'm
unsure we want to do this.
While we are a it, we include a fix on the formatter, which _must_ be
flushed before closing its associated channel.
|
|
We take inspiration and code from the Evil plugin.
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.
|
|
|
|
The issue could be reproduced by doing "dune build
test-suite/misc/universes/all_stdlib.v" (from a clean build) which
would error 127 with no message.
- only redirect stdout so that in the future we will see error
messages
- put the script as a dependency (I guess it sometime succeeded when
copying the deps for the test suite happened before running it)
|
|
We should have this in the check target, but meanwhile we have to do
manual housekeeping here.
|
|
Reviewed-by: ejgallego
|
|
- fix the printers themselves after discharge was moved to the kernel
- change the test to make it more robust
In addition to checking that there is no "Error|Unbound" in the
output, ensure that the "go" function at the end of base_include
is defined. If there are any errors in base_include it won't be defined.
This makes us find out that the test was silently failing in all CI
jobs except trunk+make. It failed to find the "include" file and so
failed with "could not find file include.", which we didn't detect.
To fix this:
- change automatically included paths in Coqinit.init_ocaml_path to be
based on coqlib instead of coqroot. This way top_printers.ml and
base_include can find the compiled ml objects.
- fix for dune: adapt the script to use include_dune when INSIDE_DUNE,
add dependencies to test-suite/dune.
The dependencies should be calculated automatically once Dune has
better support for debug, or we implement proper support for test
printers.
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
This allows to desynchronize the kernel-facing API from the proof-facing one.
|
|
|
|
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
This test is active only when configure `is_a_released_version` is set
to true. In this case, to pass the test-suite, there must be no
unreleased changelog entries left, i.e. `doc/changelog/*/` must only
contain `00000-title.rst` files.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
I think the usage looks cleaner this way.
|
|
- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files
cf https://github.com/coq/coq/issues/9464
|
|
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
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.
|
|
|
|
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
|
|
|
|
With camlp4 this file was not created but now that we use mlg it has appeared.
|
|
|
|
|
|
|
|
When launched through PATH argv.(0) is just the command name.
eg "coqtop -compile foo.v" -> argv.(0) = "coqtop"
Using executable_name also follows symlinks but this isn't tested to
avoid messing with windows. Running Coq through a symlink is not as
important as PATH anyways.
|
|
|
|
|
|
symlink from repo
|
|
Fixes #7065
|
|
|
|
|
|
|
|
|
|
|
|
The files deps-order.sh and deps-checksum.sh were concurrently rm-ing
the files of the other.
Courtesy of Guillaume M.
|
