From fad095ccc656c5fccc5e50b36067deabde233bb3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 12 Feb 2019 04:32:47 +0100 Subject: [dev] Add include versions for Dune builds. Fixes #9537 This way, users can do: ``` dune exec coqtop.byte > Drop. # #directory "dev";; # #use "include_dune";; ``` --- dev/base_include | 25 ---------------- dev/doc/build-system.dune.md | 10 +++++++ dev/inc_ltac | 7 +++++ dev/inc_ltac_dune | 7 +++++ dev/incdir | 16 +++++++++++ dev/incdir_dune | 16 +++++++++++ dev/include | 68 ++------------------------------------------ dev/include_dune | 22 ++++++++++++++ dev/include_printers | 55 +++++++++++++++++++++++++++++++++++ 9 files changed, 136 insertions(+), 90 deletions(-) create mode 100644 dev/inc_ltac create mode 100644 dev/inc_ltac_dune create mode 100644 dev/incdir create mode 100644 dev/incdir_dune create mode 100644 dev/include_dune create mode 100644 dev/include_printers diff --git a/dev/base_include b/dev/base_include index 48feeec147..b214959bad 100644 --- a/dev/base_include +++ b/dev/base_include @@ -1,24 +1,6 @@ - (* File to include to get some Coq facilities under the ocaml toplevel. This file is loaded by include *) -#cd".";; -#directory "parsing";; -#directory "interp";; -#directory "toplevel";; -#directory "library";; -#directory "kernel";; -#directory "gramlib";; -#directory "engine";; -#directory "pretyping";; -#directory "lib";; -#directory "proofs";; -#directory "tactics";; -#directory "printing";; -#directory "grammar";; -#directory "stm";; -#directory "vernac";; - #use "top_printers.ml";; #use "vm_printers.ml";; @@ -137,7 +119,6 @@ open Proof_global open Redexpr open Refiner open Tacmach -open Tactic_debug open Hints open Auto @@ -146,15 +127,9 @@ open Contradiction open Eauto open Elim open Equality -open Evar_tactics -open Extraargs -open Extratactics open Hipattern open Inv open Leminv -open Tacsubst -open Tacintern -open Tacinterp open Tacticals open Tactics open Eqschemes diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 01c32041d2..da91c85856 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -106,6 +106,16 @@ 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. +## Dropping from coqtop: + +The following sequence is recommended: +``` +dune exec coqtop.byte +> Drop. +# #directory "dev";; +# #use "include_dune";; +``` + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/inc_ltac b/dev/inc_ltac new file mode 100644 index 0000000000..8ef02445c2 --- /dev/null +++ b/dev/inc_ltac @@ -0,0 +1,7 @@ +open Evar_tactics +open Tactic_debug +open Tacsubst +open Tacintern +open Tacinterp +open Extraargs +open Extratactics diff --git a/dev/inc_ltac_dune b/dev/inc_ltac_dune new file mode 100644 index 0000000000..d7f505e8e0 --- /dev/null +++ b/dev/inc_ltac_dune @@ -0,0 +1,7 @@ +open Ltac_plugin__Evar_tactics +open Ltac_plugin__Tactic_debug +open Ltac_plugin__Tacsubst +open Ltac_plugin__Tacintern +open Ltac_plugin__Tacinterp +open Ltac_plugin__Extraargs +open Ltac_plugin__Extratactics diff --git a/dev/incdir b/dev/incdir new file mode 100644 index 0000000000..8ffd6bf6dc --- /dev/null +++ b/dev/incdir @@ -0,0 +1,16 @@ +#cd".";; +#directory "parsing";; +#directory "interp";; +#directory "toplevel";; +#directory "library";; +#directory "kernel";; +#directory "gramlib";; +#directory "engine";; +#directory "pretyping";; +#directory "lib";; +#directory "proofs";; +#directory "tactics";; +#directory "printing";; +#directory "grammar";; +#directory "stm";; +#directory "vernac";; diff --git a/dev/incdir_dune b/dev/incdir_dune new file mode 100644 index 0000000000..9d0fee1fa2 --- /dev/null +++ b/dev/incdir_dune @@ -0,0 +1,16 @@ +#cd".";; +#directory "_build/default/lib/.lib.objs/";; +#directory "_build/default/clib/.clib.objs/";; +#directory "_build/default/kernel/.kernel.objs/";; +#directory "_build/default/library/.library.objs/";; +#directory "_build/default/engine/.engine.objs/";; +#directory "_build/default/pretyping/.pretyping.objs/";; +#directory "_build/default/interp/.interp.objs/";; +#directory "_build/default/parsing/.parsing.objs/";; +#directory "_build/default/gramlib/.gramlib.objs/";; +#directory "_build/default/proofs/.proofs.objs/";; +#directory "_build/default/tactics/.tactics.objs/";; +#directory "_build/default/printing/.printing.objs/";; +#directory "_build/default/vernac/.vernac.objs/";; +#directory "_build/default/stm/.stm.objs/";; +#directory "_build/default/toplevel/.toplevel.objs/";; diff --git a/dev/include b/dev/include index c5de83b900..fa4bf827d7 100644 --- a/dev/include +++ b/dev/include @@ -1,4 +1,3 @@ - (* File to include to install the pretty-printers in the ocaml toplevel *) (* Typical usage : @@ -15,69 +14,8 @@ then ignore (Toploop.use_silently Format.std_formatter "dev/include") *) -(* For OCaml 3.10.x: - clflags.cmi (a ocaml compilation by-product) must be in the library path. - On Debian, install ocaml-compiler-libs, and uncomment the following: - #directory "+compiler-libs/utils";; - Clflags.recursive_types := true;; -*) - #cd ".";; +#use "incdir";; #use "base_include";; - -#install_printer (* pp_stdcmds *) pp;; - -#install_printer (* pattern *) pppattern;; -#install_printer (* glob_constr *) ppglob_constr;; -#install_printer (* open constr *) ppopenconstr;; -#install_printer (* constr *) ppconstr;; -#install_printer (* econstr *) ppeconstr;; -#install_printer (* constr_substituted *) ppsconstr;; -#install_printer (* constraints *) ppconstraints;; -#install_printer (* univ constraints *) ppuniverseconstraints;; -#install_printer (* universe *) ppuni;; -#install_printer (* universes *) ppuniverses;; -#install_printer (* univ level *) ppuni_level;; -#install_printer (* univ context *) ppuniverse_context;; -#install_printer (* univ context future *) ppuniverse_context_future;; -#install_printer (* univ context set *) ppuniverse_context_set;; -#install_printer (* univ set *) ppuniverse_set;; -#install_printer (* univ instance *) ppuniverse_instance;; -#install_printer (* univ subst *) ppuniverse_subst;; -#install_printer (* univ full subst *) ppuniverse_level_subst;; -#install_printer (* univ opt subst *) ppuniverse_opt_subst;; -#install_printer (* evar univ ctx *) ppevar_universe_context;; -#install_printer (* inductive *) ppind;; -#install_printer (* 'a scheme_kind *) ppscheme;; -#install_printer (* type_judgement *) pptype;; -#install_printer (* judgement *) ppj;; -#install_printer (* id set *) ppidset;; -#install_printer (* int set *) ppintset;; - -#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; -#install_printer (* Reductionops machine stack *) pp_stack_t;; - -(*#install_printer (* hint_db *) print_hint_db;;*) -(*#install_printer (* hints_path *) pphintspath;;*) -#install_printer (* goal *) ppgoal;; -(*#install_printer (* sigma goal *) ppsigmagoal;;*) -#install_printer (* proof *) pproof;; -#install_printer (* Goal.goal *) ppgoalgoal;; -#install_printer (* proofview *) ppproofview;; -#install_printer (* metaset.t *) ppmetas;; -#install_printer (* evar *) ppevar;; -#install_printer (* evar_map *) ppevm;; -#install_printer (* Evar.Set.t *) ppexistentialset;; -#install_printer (* clenv *) ppclenv;; -#install_printer (* env *) ppenv;; -#install_printer (* Hint_db.t *) pphintdb;; -#install_printer (* named_context_val *) ppnamedcontextval;; - -#install_printer (* tactic *) pptac;; -#install_printer (* object *) ppobj;; -#install_printer (* global_reference *) ppglobal;; -#install_printer (* generic_argument *) pp_generic_argument;; - -#install_printer (* fconstr *) ppfconstr;; - -#install_printer (* Future.computation *) ppfuture;; +#use "inc_ltac";; +#use "include_printers";; diff --git a/dev/include_dune b/dev/include_dune new file mode 100644 index 0000000000..2ef8eb4d04 --- /dev/null +++ b/dev/include_dune @@ -0,0 +1,22 @@ +(* File to include to install the pretty-printers in the ocaml toplevel *) + +(* Typical usage : + + $ dune exec coqtop.byte # or even better : rlwrap coqtop.byte + Coq < Drop. + # #directory "dev";; + # #use "include";; + + Alternatively, you can avoid typing #use "include" after each Drop + by adding the following lines in your $HOME/.ocamlinit : + + #directory "+compiler-libs";; + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "dev/include") +*) + +#cd ".";; +#use "incdir_dune";; +#use "base_include";; +#use "inc_ltac_dune";; +#use "include_printers";; diff --git a/dev/include_printers b/dev/include_printers new file mode 100644 index 0000000000..90088e40bf --- /dev/null +++ b/dev/include_printers @@ -0,0 +1,55 @@ +#install_printer (* pp_stdcmds *) pp;; +#install_printer (* pattern *) pppattern;; +#install_printer (* glob_constr *) ppglob_constr;; +#install_printer (* open constr *) ppopenconstr;; +#install_printer (* constr *) ppconstr;; +#install_printer (* econstr *) ppeconstr;; +#install_printer (* constr_substituted *) ppsconstr;; +#install_printer (* constraints *) ppconstraints;; +#install_printer (* univ constraints *) ppuniverseconstraints;; +#install_printer (* universe *) ppuni;; +#install_printer (* universes *) ppuniverses;; +#install_printer (* univ level *) ppuni_level;; +#install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context future *) ppuniverse_context_future;; +#install_printer (* univ context set *) ppuniverse_context_set;; +#install_printer (* univ set *) ppuniverse_set;; +#install_printer (* univ instance *) ppuniverse_instance;; +#install_printer (* univ subst *) ppuniverse_subst;; +#install_printer (* univ full subst *) ppuniverse_level_subst;; +#install_printer (* univ opt subst *) ppuniverse_opt_subst;; +#install_printer (* evar univ ctx *) ppevar_universe_context;; +#install_printer (* inductive *) ppind;; +#install_printer (* 'a scheme_kind *) ppscheme;; +#install_printer (* type_judgement *) pptype;; +#install_printer (* judgement *) ppj;; +#install_printer (* id set *) ppidset;; +#install_printer (* int set *) ppintset;; + +#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; +#install_printer (* Reductionops machine stack *) pp_stack_t;; + +(*#install_printer (* hint_db *) print_hint_db;;*) +(*#install_printer (* hints_path *) pphintspath;;*) +#install_printer (* goal *) ppgoal;; +(*#install_printer (* sigma goal *) ppsigmagoal;;*) +#install_printer (* proof *) pproof;; +#install_printer (* Goal.goal *) ppgoalgoal;; +#install_printer (* proofview *) ppproofview;; +#install_printer (* metaset.t *) ppmetas;; +#install_printer (* evar *) ppevar;; +#install_printer (* evar_map *) ppevm;; +#install_printer (* Evar.Set.t *) ppexistentialset;; +#install_printer (* clenv *) ppclenv;; +#install_printer (* env *) ppenv;; +#install_printer (* Hint_db.t *) pphintdb;; +#install_printer (* named_context_val *) ppnamedcontextval;; + +#install_printer (* tactic *) pptac;; +#install_printer (* object *) ppobj;; +#install_printer (* global_reference *) ppglobal;; +#install_printer (* generic_argument *) pp_generic_argument;; + +#install_printer (* fconstr *) ppfconstr;; + +#install_printer (* Future.computation *) ppfuture;; -- cgit v1.2.3