| 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.
|
|
AFAICT `echo "$(pwd)"` is unsound for the dune cache when called from
different paths (typically different git worktrees).
|
|
We only want stdout, so if there's something in stderr it will both
make a wrong output and make it harder to debug.
|
|
The quoting was incorrect thus scripts didn't properly work.
|
|
We add a shim for running the byte version of coqtop. This fixes the
Coq part of #9727 , the Dune part is still open at
https://github.com/ocaml/dune/issues/108 but this PR includes a
workaround.
Unfortunately we have to introduce a small inefficiency in the build
process as we build both byte and native versions of plugins for this
work reliable.
As this is a choice done during bootstrap it won't be easy to fix
until we have our own `dune coqtop` command and we can control the
rules depending on the final target.
This should affect the `check` target so still fast builds should be
possible, but if this is a problem we could add a `byteboot` target to
help.
|
|
As requested by Gaëtan Gilbert, we add shims
- `dev/shim/coqtop-prelude`
- `dev/shim/coqide-prelude`
that will build and start `coqtop` and `coqide` with just the prelude
loaded properly.
`dune exec dev/shim/coqtop-prelude` will build and execute this shim,
equivalent to doing `make states && bin/coqtop` under the old model.
This PR is just a bit of "a hack" until proper support for Coq
libraries arrives to Dune, however there is nothing wrong with it.
In particular, we must bootstrap `coq.plugins.ltac` as Dune needs to
compute the full installation path to allow `%{bin:foo}` in deps,
[this is a kind of shortcoming of the current implementation, and the
error message is just terrible]
We cannot depend on installed `.vo` files without doing a gross hack
[including them inside an ml lib] so for now we just depend on their
non-installed forms. Using `%{bin}` is good enough for the shims who
would like to locate binaries using `PATH`.
The long term plan (for now) is to have a command similar to `dune
utop $dir`, `dune coqtop $dir`, which would spawn a proper Coq shell
with the corresponding libraries on the path.
This will work for `dir=stdlib/Init/` for example, or for any other
combination.
|
