diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 25 | ||||
| -rw-r--r-- | dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh | 12 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 3 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 10 | ||||
| -rw-r--r-- | dev/inc_ltac | 7 | ||||
| -rw-r--r-- | dev/inc_ltac_dune | 7 | ||||
| -rw-r--r-- | dev/incdir | 16 | ||||
| -rw-r--r-- | dev/incdir_dune | 16 | ||||
| -rw-r--r-- | dev/include | 68 | ||||
| -rw-r--r-- | dev/include_dune | 22 | ||||
| -rw-r--r-- | dev/include_printers | 55 |
11 files changed, 151 insertions, 90 deletions
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/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh new file mode 100644 index 0000000000..27ce9aca16 --- /dev/null +++ b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then + + equations_CI_REF=hooks_unify + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=hooks_unify + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=hooks_unify + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 5705857d76..3f1b470878 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -37,6 +37,9 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. +To know what files you are a code owner of in a large PR, you can run +`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect. + When a PR received lots of comments or if the PR has not been opened for long and the assignee thinks that some other developers might want to comment, it is recommended that they announce their intention to merge and wait a full 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;; |