diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_db | 1 | ||||
| -rw-r--r-- | dev/checker.dbg | 1 | ||||
| -rw-r--r-- | dev/checker_db | 36 | ||||
| -rw-r--r-- | dev/checker_dune_db | 5 | ||||
| -rw-r--r-- | dev/checker_printers.dbg | 35 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 6 | ||||
| -rw-r--r-- | dev/core.dbg | 4 | ||||
| -rw-r--r-- | dev/core_dune.dbg | 20 | ||||
| -rw-r--r-- | dev/db | 88 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 21 | ||||
| -rw-r--r-- | dev/dune | 25 | ||||
| -rwxr-xr-x | dev/dune-dbg.in | 11 | ||||
| -rw-r--r-- | dev/dune-workspace.all | 2 | ||||
| -rw-r--r-- | dev/dune_db | 6 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 85 |
15 files changed, 220 insertions, 126 deletions
diff --git a/dev/base_db b/dev/base_db index e18ac534ac..155e9591e0 100644 --- a/dev/base_db +++ b/dev/base_db @@ -1,4 +1,5 @@ source core.dbg +load_printer ltac_plugin.cmo load_printer top_printers.cmo install_printer Top_printers.ppid install_printer Top_printers.ppsp diff --git a/dev/checker.dbg b/dev/checker.dbg index b2323b6175..b5b7f0e6d3 100644 --- a/dev/checker.dbg +++ b/dev/checker.dbg @@ -2,5 +2,6 @@ load_printer threads.cma load_printer str.cma load_printer clib.cma load_printer dynlink.cma +load_printer config.cma load_printer lib.cma load_printer check.cma diff --git a/dev/checker_db b/dev/checker_db index 327e636c57..fcb6f679ed 100644 --- a/dev/checker_db +++ b/dev/checker_db @@ -2,38 +2,4 @@ source checker.dbg load_printer checker_printers.cmo -install_printer Checker_printers.pP - -install_printer Checker_printers.ppfuture - -install_printer Checker_printers.ppid -install_printer Checker_printers.pplab -install_printer Checker_printers.ppmbid -install_printer Checker_printers.ppdir -install_printer Checker_printers.ppmp -install_printer Checker_printers.ppcon -install_printer Checker_printers.ppproj -install_printer Checker_printers.ppkn -install_printer Checker_printers.ppmind -install_printer Checker_printers.ppind - -install_printer Checker_printers.ppbigint - -install_printer Checker_printers.ppintset -install_printer Checker_printers.ppidset - -install_printer Checker_printers.ppidmapgen - -install_printer Checker_printers.ppididmap - -install_printer Checker_printers.ppuni -install_printer Checker_printers.ppuni_level -install_printer Checker_printers.ppuniverse_set -install_printer Checker_printers.ppuniverse_instance -install_printer Checker_printers.ppauniverse_context -install_printer Checker_printers.ppuniverse_context -install_printer Checker_printers.ppconstraints -install_printer Checker_printers.ppuniverse_context_future -install_printer Checker_printers.ppuniverses - -install_printer Checker_printers.pploc +source checker_printers.dbg diff --git a/dev/checker_dune_db b/dev/checker_dune_db new file mode 100644 index 0000000000..cdb6a4b809 --- /dev/null +++ b/dev/checker_dune_db @@ -0,0 +1,5 @@ +source checker_dune.dbg + +load_printer checker_printers.cma + +source checker_printers.dbg diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg new file mode 100644 index 0000000000..9ebbd74834 --- /dev/null +++ b/dev/checker_printers.dbg @@ -0,0 +1,35 @@ +install_printer Checker_printers.pP + +install_printer Checker_printers.ppfuture + +install_printer Checker_printers.ppid +install_printer Checker_printers.pplab +install_printer Checker_printers.ppmbid +install_printer Checker_printers.ppdir +install_printer Checker_printers.ppmp +install_printer Checker_printers.ppcon +install_printer Checker_printers.ppproj +install_printer Checker_printers.ppkn +install_printer Checker_printers.ppmind +install_printer Checker_printers.ppind + +install_printer Checker_printers.ppbigint + +install_printer Checker_printers.ppintset +install_printer Checker_printers.ppidset + +install_printer Checker_printers.ppidmapgen + +install_printer Checker_printers.ppididmap + +install_printer Checker_printers.ppuni +install_printer Checker_printers.ppuni_level +install_printer Checker_printers.ppuniverse_set +install_printer Checker_printers.ppuniverse_instance +install_printer Checker_printers.ppauniverse_context +install_printer Checker_printers.ppuniverse_context +install_printer Checker_printers.ppconstraints +install_printer Checker_printers.ppuniverse_context_future +install_printer Checker_printers.ppuniverses + +install_printer Checker_printers.pploc diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 41e1d1a937..098c950b32 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-22-V1" +# CACHEKEY: "bionic_coq-V2018-10-23-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ 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.0 dune.1.2.1 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. @@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/core.dbg b/dev/core.dbg index 972ba701e4..f676b643e4 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,6 +1,7 @@ -source camlp5.dbg load_printer threads.cma load_printer str.cma +load_printer gramlib.cma +load_printer config.cma load_printer clib.cma load_printer dynlink.cma load_printer lib.cma @@ -16,4 +17,3 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer ltac_plugin.cmo diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg new file mode 100644 index 0000000000..cf9c5bd39a --- /dev/null +++ b/dev/core_dune.dbg @@ -0,0 +1,20 @@ +load_printer threads.cma +load_printer str.cma +load_printer gramlib.cma +load_printer config.cma +load_printer clib.cma +load_printer dynlink.cma +load_printer lib.cma +load_printer byterun.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +load_printer proofs.cma +load_printer parsing.cma +load_printer printing.cma +load_printer tactics.cma +load_printer vernac.cma +load_printer stm.cma +load_printer toplevel.cma @@ -1,88 +1,6 @@ source core.dbg + +load_printer ltac_plugin.cmo load_printer top_printers.cmo -install_printer Top_printers.pP -install_printer Top_printers.ppfuture -install_printer Top_printers.ppid -install_printer Top_printers.pplab -install_printer Top_printers.ppmbid -install_printer Top_printers.ppdir -install_printer Top_printers.ppmp -install_printer Top_printers.ppcon -install_printer Top_printers.ppproj -install_printer Top_printers.ppkn -install_printer Top_printers.ppmind -install_printer Top_printers.ppind -install_printer Top_printers.ppsp -install_printer Top_printers.ppqualid -install_printer Top_printers.ppclindex -install_printer Top_printers.ppscheme -install_printer Top_printers.ppwf_paths -install_printer Top_printers.ppevar -install_printer Top_printers.ppconstr -install_printer Top_printers.ppsconstr -install_printer Top_printers.ppeconstr -install_printer Top_printers.ppconstr_expr -install_printer Top_printers.ppglob_constr -install_printer Top_printers.pppattern -install_printer Top_printers.ppfconstr -install_printer Top_printers.ppbigint -install_printer Top_printers.ppintset -install_printer Top_printers.ppidset -install_printer Top_printers.ppidmapgen -install_printer Top_printers.ppididmap -install_printer Top_printers.ppconstrunderbindersidmap -install_printer Top_printers.ppevarsubst -install_printer Top_printers.ppunbound_ltac_var_map -install_printer Top_printers.ppclosure -install_printer Top_printers.ppclosedglobconstr -install_printer Top_printers.ppclosedglobconstridmap -install_printer Top_printers.ppglobal -install_printer Top_printers.ppconst -install_printer Top_printers.ppvar -install_printer Top_printers.ppj -install_printer Top_printers.ppsubst -install_printer Top_printers.ppdelta -install_printer Top_printers.pp_idpred -install_printer Top_printers.pp_cpred -install_printer Top_printers.pp_transparent_state -install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t -install_printer Top_printers.pp_state_t -install_printer Top_printers.ppmetas -install_printer Top_printers.ppevm -install_printer Top_printers.ppexistentialset -install_printer Top_printers.ppexistentialfilter -install_printer Top_printers.ppclenv -install_printer Top_printers.ppgoalgoal -install_printer Top_printers.ppgoal -install_printer Top_printers.pphintdb -install_printer Top_printers.ppproofview -install_printer Top_printers.ppopenconstr -install_printer Top_printers.pproof -install_printer Top_printers.ppuni -install_printer Top_printers.ppuni_level -install_printer Top_printers.ppuniverse_set -install_printer Top_printers.ppuniverse_instance -install_printer Top_printers.ppuniverse_context -install_printer Top_printers.ppuniverse_context_set -install_printer Top_printers.ppuniverse_subst -install_printer Top_printers.ppuniverse_opt_subst -install_printer Top_printers.ppuniverse_level_subst -install_printer Top_printers.ppevar_universe_context -install_printer Top_printers.ppconstraints -install_printer Top_printers.ppuniverseconstraints -install_printer Top_printers.ppuniverse_context_future -install_printer Top_printers.ppcumulativity_info -install_printer Top_printers.ppabstract_cumulativity_info -install_printer Top_printers.ppuniverses -install_printer Top_printers.ppnamedcontextval -install_printer Top_printers.ppenv -install_printer Top_printers.pptac -install_printer Top_printers.ppobj -install_printer Top_printers.pploc -install_printer Top_printers.pp_argument_type -install_printer Top_printers.pp_generic_argument -install_printer Top_printers.ppgenarginfo -install_printer Top_printers.ppgenargargt -install_printer Top_printers.ppist +source top_printers.dbg diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 91ab57f1e9..0aeb30c4e8 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -68,6 +68,27 @@ Note that you must invoke the `#rectypes;;` toplevel flag in order to use Coq libraries. The provided `.ocamlinit` file does this automatically. +## ocamldebug + +You can use `ocamldebug` with Dune; after a build, do: + +``` +dune exec dev/dune-dbg +(ocd) source dune_db +``` + +or + +``` +dune exec dev/dune-dbg checker +(ocd) source checker_dune_db +``` + +for the checker. 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. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/dune b/dev/dune new file mode 100644 index 0000000000..fd6c8cf32c --- /dev/null +++ b/dev/dune @@ -0,0 +1,25 @@ +(library + (name top_printers) + (public_name coq.top_printers) + (synopsis "Coq's Debug Printers") + (wrapped false) + (modules :standard \ checker_printers) + (libraries coq.toplevel coq.plugins.ltac)) + +(library + (name checker_printers) + (public_name coq.checker_printers) + (synopsis "Coq's Debug Printers [for the Checker]") + (wrapped false) + (flags :standard -open Checklib) + (modules checker_printers) + (libraries coq.checklib)) + +(rule + (targets dune-dbg) + (deps dune-dbg.in + ../checker/main.bc + ../topbin/coqtop_byte_bin.bc + ; This is not enough as the call to `ocamlfind` will fail :/ + top_printers.cma) + (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in new file mode 100755 index 0000000000..464e026400 --- /dev/null +++ b/dev/dune-dbg.in @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +# Run in a proper install dune env. +case $1 in +checker) + ocamldebug `ocamlfind query -recursive -i-format coq.checker_printers` -I +threads -I dev _build/default/checker/main.bc + ;; +*) + ocamldebug `ocamlfind query -recursive -i-format coq.top_printers` -I +threads -I dev _build/default/topbin/coqtop_byte_bin.bc + ;; +esac diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 93b807d5e3..f45f6de529 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,4 +1,4 @@ -(lang dune 1.2) +(lang dune 1.4) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) diff --git a/dev/dune_db b/dev/dune_db new file mode 100644 index 0000000000..f920f7c75c --- /dev/null +++ b/dev/dune_db @@ -0,0 +1,6 @@ +source core_dune.dbg + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg new file mode 100644 index 0000000000..eab88c7290 --- /dev/null +++ b/dev/top_printers.dbg @@ -0,0 +1,85 @@ +install_printer Top_printers.pP +install_printer Top_printers.ppfuture +install_printer Top_printers.ppid +install_printer Top_printers.pplab +install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir +install_printer Top_printers.ppmp +install_printer Top_printers.ppcon +install_printer Top_printers.ppproj +install_printer Top_printers.ppkn +install_printer Top_printers.ppmind +install_printer Top_printers.ppind +install_printer Top_printers.ppsp +install_printer Top_printers.ppqualid +install_printer Top_printers.ppclindex +install_printer Top_printers.ppscheme +install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppevar +install_printer Top_printers.ppconstr +install_printer Top_printers.ppsconstr +install_printer Top_printers.ppeconstr +install_printer Top_printers.ppconstr_expr +install_printer Top_printers.ppglob_constr +install_printer Top_printers.pppattern +install_printer Top_printers.ppfconstr +install_printer Top_printers.ppbigint +install_printer Top_printers.ppintset +install_printer Top_printers.ppidset +install_printer Top_printers.ppidmapgen +install_printer Top_printers.ppididmap +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppevarsubst +install_printer Top_printers.ppunbound_ltac_var_map +install_printer Top_printers.ppclosure +install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppclosedglobconstridmap +install_printer Top_printers.ppglobal +install_printer Top_printers.ppconst +install_printer Top_printers.ppvar +install_printer Top_printers.ppj +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta +install_printer Top_printers.pp_idpred +install_printer Top_printers.pp_cpred +install_printer Top_printers.pp_transparent_state +install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.pp_state_t +install_printer Top_printers.ppmetas +install_printer Top_printers.ppevm +install_printer Top_printers.ppexistentialset +install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppclenv +install_printer Top_printers.ppgoalgoal +install_printer Top_printers.ppgoal +install_printer Top_printers.pphintdb +install_printer Top_printers.ppproofview +install_printer Top_printers.ppopenconstr +install_printer Top_printers.pproof +install_printer Top_printers.ppuni +install_printer Top_printers.ppuni_level +install_printer Top_printers.ppuniverse_set +install_printer Top_printers.ppuniverse_instance +install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppuniverse_context_set +install_printer Top_printers.ppuniverse_subst +install_printer Top_printers.ppuniverse_opt_subst +install_printer Top_printers.ppuniverse_level_subst +install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuniverseconstraints +install_printer Top_printers.ppuniverse_context_future +install_printer Top_printers.ppcumulativity_info +install_printer Top_printers.ppabstract_cumulativity_info +install_printer Top_printers.ppuniverses +install_printer Top_printers.ppnamedcontextval +install_printer Top_printers.ppenv +install_printer Top_printers.pptac +install_printer Top_printers.ppobj +install_printer Top_printers.pploc +install_printer Top_printers.pp_argument_type +install_printer Top_printers.pp_generic_argument +install_printer Top_printers.ppgenarginfo +install_printer Top_printers.ppgenargargt +install_printer Top_printers.ppist |