| Age | Commit message (Collapse) | Author |
|---|
|
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
|
|
This is not used anymore, and after #14122 the makefile parts for the
dmg generation are not used anymore.
Closes #7476 .
|
|
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: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.
|
|
|
|
instead of recursive make
|
|
C functions were used for floating-point arithmetic operations, by
fear of double rounding that could happen on old x87 on 32 bits
architecture. This commit uses OCaml floating-point operations on 64
bits architectures.
The following snippet is made 17% faster by this commit.
From Coq Require Import Int63 BinPos PrimFloat.
Definition foo n :=
let eps := sub (next_up one) one in
Pos.iter (fun x => add x eps) two n.
Time Eval native_compute in foo 1000000000.
|
|
|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
Add headers to a few files which were missing them.
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
PR #11267 reverted commit d21e17ac99dfb2008f2e2bfdb373413490d1ffc7 (of
PR #10695) by error, this reinstates it.
|
|
Fix #11266
|
|
|
|
Picked from #8729. This should help preserve the history better when
we split.
|
