diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/11051-gares-elpi-1.8.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/11708-gares-elpi-1.10.sh | 6 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 36 | ||||
| -rw-r--r-- | dev/dune | 38 |
6 files changed, 70 insertions, 28 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index b8f9d99702..41392b4b8c 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-12-08-V82" +# CACHEKEY: "bionic_coq-V2019-03-01-V43" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,9 +37,9 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.0.8 odoc.1.4.2" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.8.0" + BASE_ONLY_OPAM="elpi.1.10.2" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" diff --git a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh deleted file mode 100644 index 7845654375..0000000000 --- a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11051" ] || [ "$CI_BRANCH" = "elpi-1.8" ]; then - - elpi_CI_REF="coq-master+v1.2" - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh new file mode 100644 index 0000000000..8b0f86d951 --- /dev/null +++ b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11602" ] || [ "$CI_BRANCH" = "master+support-only-parsing-where-clause" ]; then + + equations_CI_REF=master+adapt-coq-pr11602-only-parsing-where-notation + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/11708-gares-elpi-1.10.sh b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh new file mode 100644 index 0000000000..121190e5f6 --- /dev/null +++ b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11708" ] || [ "$CI_BRANCH" = " elpi-1.10+coq-elpi-1.3" ]; then + + elpi_CI_REF="coq-master+coq-elpi-1.3" + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index cd35064b18..0506216541 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -46,21 +46,27 @@ of build threads `(jobs N)` and display options `(display _mode_)`. ## Running binaries [coqtop / coqide] -There are two special targets `states` and `quickide` that will -generate "shims" for running `coqtop` and `coqide` in a fast build. In -order to use them, do: +Running `coqtop` directly with `dune exec -- coqtop` won't in general +work well unless you are using `dune exec -- coqtop -noinit`. The +`coqtop` binary doesn't depend itself on Coq's prelude, so plugins / +vo files may go stale if you rebuild only `coqtop`. + +Instead, you should use the provided "shims" for running `coqtop` and +`coqide` in a fast build. In order to use them, do: ``` $ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` -or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets -enjoy quick incremental compilation thanks to `-opaque` so they tend -to be very fast while developing. +or `quickide` / `dev/shim/coqide-prelude` for CoqIDE, etc.... See +`dev/shim/dune` for a complete list of targets. These targets enjoy +quick incremental compilation thanks to `-opaque` so they tend to be +very fast while developing. Note that for a fast developer build of ML files, the `check` target -will be faster. +is faster, as it doesn't link the binaries and uses the non-optimizing +compiler. ## Targets @@ -119,10 +125,9 @@ dune exec -- dev/dune-dbg checker foo.vo (ocd) source dune_db ``` -Unfortunately, dependency handling here is not fully refined, so you -need to build enough of Coq once to use this target [it will then -correctly compute the deps and rebuild if you call the script again] -This will be fixed in the future. +Unfortunately, dependency handling is not fully refined / automated, +you may find the occasional hiccup due to libraries being renamed, +etc... Please report any issue. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. @@ -214,3 +219,12 @@ useful to Coq, some examples are: - Cross-compilation. - Automatic Generation of OPAM files. - Multi-directory libraries. + +## FAQ + +- I get "Error: Dynlink error: Interface mismatch": + + You are likely running a partial build which doesn't include + implicitly loaded plugins / vo files. See the "Running binaries + [coqtop / coqide]" section above as to how to correctly call Coq's + binaries. @@ -9,12 +9,34 @@ (rule (targets dune-dbg) - (deps dune-dbg.in - ../checker/coqchk.bc - ../topbin/coqc_bin.bc - ../ide/coqide_main.bc - %{lib:coq.plugins.ltac:ltac_plugin.cma} - ; This is not enough, the call to `ocamlfind` may fail if the - ; META file is not yet in place :/ - top_printers.cma) + (deps + dune-dbg.in + ../checker/coqchk.bc + ../topbin/coqc_bin.bc + ../ide/coqide_main.bc + ; We require all the OCaml libs to be in place and searchable + ; by OCamlfind, this is a bit of a hack but until Dune gets + ; proper ocamldebug support we have to live with that. + %{lib:coq.config:config.cma} + %{lib:coq.clib:clib.cma} + %{lib:coq.lib:lib.cma} + %{lib:coq.kernel:kernel.cma} + %{lib:coq.vm:byterun.cma} + %{lib:coq.vm:../../stublibs/dllbyterun_stubs.so} + %{lib:coq.library:library.cma} + %{lib:coq.engine:engine.cma} + %{lib:coq.pretyping:pretyping.cma} + %{lib:coq.gramlib:gramlib.cma} + %{lib:coq.interp:interp.cma} + %{lib:coq.proofs:proofs.cma} + %{lib:coq.parsing:parsing.cma} + %{lib:coq.printing:printing.cma} + %{lib:coq.tactics:tactics.cma} + %{lib:coq.vernac:vernac.cma} + %{lib:coq.stm:stm.cma} + %{lib:coq.toplevel:toplevel.cma} + %{lib:coq.plugins.ltac:ltac_plugin.cma} + %{lib:coq.top_printers:top_printers.cmi} + %{lib:coq.top_printers:top_printers.cma} + %{lib:coq.top_printers:../META}) (action (copy dune-dbg.in dune-dbg))) |