| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
Reviewed-by: ejgallego
|
|
|
|
instead of recursive make
|
|
(for runs outside dune, ie "make -C test-suite unit-tests" rather than
"dune build @runtest")
Fix #13333
|
|
- merlin.in : added zarith
- test-suite/Makefile remove .csdp.cache on make clean
updated .csdp.cache.test-suite
|
|
Reviewed-by: ejgallego
|
|
documentation
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle
|
|
Reviewed-by: SkySkimmer
|
|
It now silently does nothing rather than erroring with `mv: cannot stat
'output/*.out.real': No such file or directory` if there is no output to
approve, and also correctly handles `output-coqtop` and `output-coqchk`
rather than ignoring these directories.
Fixes #12863
|
|
test files.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
The directory is obsolete since 7461fe4f.
|
|
OUnit package name is changed from "oUnit" to "ounit2":
https://github.com/gildor478/ounit#user-content-transition-to-ounit2
This change follows it and fixes
a failure, `ocamlfind: Package oUnit not found`,
at `make test-suite` and `dune build`.
|
|
Fix #12742
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Fixes #12582
The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should
be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says
that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime
`plik.v.log` is older than `Nat.vo`. This is circular, and results in
`make` considering all of the `modules/` tests out-of-date on any fresh
run.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: herbelin
|
|
This is needed for the case the sources are set to read-only mode, for
example when using Dune >= 2.5 [needed for the global cache support]
Fixes #12264
Co-authored-by: Ignat Insarov <kindaro@gmail.com>
|
|
|
|
This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and
0976a670cf853c9bc61b3eee6dceae4a429e066f.
|
|
Since `ocaml_pwd.ml` was added this unquoted glob would be expanded by
the shell before being passed to `find`.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
|
|
Add headers to a few files which were missing them.
|
|
This was accidentaly disabled by #6264 when no_native_compiler was
renamed to native_compiler.
Moreover, the (then unactivated test) was broken by commit 48ae6ce
(part of #9088).
|
|
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
(and not just…
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
The regexp parsing the time needed an update to support the case
"Finished failing translation". Also, not all cases of failures were
reported.
|
|
|
|
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
|
|
Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where
it fails with "syntax error". Similarly for `-` and `/`.
|
|
This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734.
A better fix is coming
|
|
Apparently the bogomips produced by cygwin are extra-bogo.
|
|
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.
|
|
In particular, display how long they took in bogomips-adjusted
centiseconds.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
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.
|
|
Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.
Also move primitive integer tests to place all primitive tests in the
same directory.
|
|
i.e. you can do
~~~
make -f Makefile.dune world
make -C test-suite success
~~~
to make just the success tests, then modify Coq sources and retest
just the ones you want
|
|
with coqtop
Reviewed-by: gares
Ack-by: jfehrle
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
