aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include3
-rw-r--r--dev/ci/ci-basic-overlay.sh12
-rwxr-xr-xdev/ci/ci-bignums.sh2
-rwxr-xr-xdev/ci/ci-equations.sh10
-rwxr-xr-xdev/ci/ci-ltac2.sh10
-rw-r--r--dev/db1
-rw-r--r--dev/doc/debugging.md7
-rwxr-xr-xdev/tools/should-check-whitespace.sh2
-rw-r--r--dev/top_printers.ml68
-rw-r--r--dev/vm_printers.ml8
10 files changed, 81 insertions, 42 deletions
diff --git a/dev/base_include b/dev/base_include
index f2912e1127..1da5e3ed18 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -130,7 +130,6 @@ open Reserve
open Syntax_def
open Constrexpr
open Constrexpr_ops
-open Topconstr
open Notation_term
open Notation_ops
open Prettyp
@@ -231,7 +230,7 @@ let pf_e gl s =
let _ = Flags.in_debugger := false
let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
- (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+ (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 59a71b6086..168a34e6e4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -53,6 +53,12 @@
: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
########################################################################
+# Ltac2
+########################################################################
+: ${ltac2_CI_BRANCH:=master}
+: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}
+
+########################################################################
# GeoCoq
########################################################################
: ${GeoCoq_CI_BRANCH:=master}
@@ -129,3 +135,9 @@
########################################################################
: ${bignums_CI_BRANCH:=master}
: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
+
+########################################################################
+# Equations
+########################################################################
+: ${Equations_CI_BRANCH:=8.8+alpha}
+: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index ff5935d4c7..d68674381a 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
# This script could be included inside other ones
# Let's avoid to source ci-common twice in this case
-if [ -z "${CI_BUILD_DIR}"];
+if [ -z "${CI_BUILD_DIR}" ];
then
source ${ci_dir}/ci-common.sh
fi
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
new file mode 100755
index 0000000000..f7470463d9
--- /dev/null
+++ b/dev/ci/ci-equations.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Equations_CI_DIR=${CI_BUILD_DIR}/Equations
+
+git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR}
+
+( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install)
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
new file mode 100755
index 0000000000..4865be31ec
--- /dev/null
+++ b/dev/ci/ci-ltac2.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+
+git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR}
+
+( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install )
diff --git a/dev/db b/dev/db
index a5518e3c4a..24ae3957ef 100644
--- a/dev/db
+++ b/dev/db
@@ -68,5 +68,6 @@ install_printer Top_printers.ppist
install_printer Top_printers.ppconstrunderbindersidmap
install_printer Top_printers.ppunbound_ltac_var_map
install_printer Top_printers.ppididmap
+install_printer Top_printers.ppidmapgen
install_printer Top_printers.ppclosure
install_printer Top_printers.ppclosedglobconstr
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index 7e9373b294..7d3d811cc3 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -54,9 +54,10 @@ Debugging from Caml debugger
of each of error* functions or anomaly* functions in lib/util.ml
- If "source db" fails, do a "make printers" and try again (it should build
top_printers.cmo and the core cma files).
- - If you have the OCAMLRUNPARAM environment variable set, Coq may hang on
- startup when run from the debugger. If this happens, unset the variable,
- re-start Emacs, and run the debugger again.
+ - If you build Coq with an OCaml version earlier than 4.06, and have the
+ OCAMLRUNPARAM environment variable set, Coq may hang on startup when run
+ from the debugger. If this happens, unset the variable, re-start Emacs, and
+ run the debugger again.
Global gprof-based profiling
============================
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
index 8159506b41..190511d957 100755
--- a/dev/tools/should-check-whitespace.sh
+++ b/dev/tools/should-check-whitespace.sh
@@ -2,4 +2,4 @@
# determine if a file has whitespace checking enabled in .gitattributes
-git check-attr whitespace -- "$1" | grep -q -v 'unspecified$'
+git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$'
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 35956477df..0f496d3b9f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,16 +8,16 @@
(* Printers for the ocaml toplevel. *)
+open Sorts
open Util
open Pp
open Names
open Libnames
open Globnames
-open Nameops
open Univ
open Environ
open Printer
-open Term
+open Constr
open Evd
open Goptions
open Genarg
@@ -37,15 +37,15 @@ let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
(* name printers *)
let ppid id = pp (Id.print id)
-let pplab l = pp (pr_lab l)
+let pplab l = pp (Label.print l)
let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
let ppdir dir = pp (pr_dirpath dir)
let ppmp mp = pp(str (ModPath.debug_to_string mp))
-let ppcon con = pp(debug_pr_con con)
-let ppproj con = pp(debug_pr_con (Projection.constant con))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
let ppkn kn = pp(str (KerName.to_string kn))
-let ppmind kn = pp(debug_pr_mind kn)
-let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
let ppsp sp = pp(pr_path sp)
let ppqualid qid = pp(pr_qualid qid)
let ppclindex cl = pp(Classops.pr_cl_index cl)
@@ -60,6 +60,7 @@ let pprecarg = function
let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
(* term printers *)
+let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
let rawdebug = ref false
let ppevar evk = pp (str (Evd.string_of_existential evk))
let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
@@ -69,9 +70,9 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.o
let ppterm = ppconstr
let ppsconstr x = ppconstr (Mod_subst.force_constr x)
let ppconstr_univ x = Constrextern.with_universes ppconstr x
-let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
-let pppattern = (fun x -> pp(pr_constr_pattern x))
-let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
+let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
+let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
+let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
let ppbigint n = pp (str (Bigint.to_string n));;
@@ -85,9 +86,14 @@ let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
let pridmap pr l =
let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
-
let ppidmap pr l = pp (pridmap pr l)
+let pridmapgen l =
+ let dom = Id.Set.elements (Id.Map.domain l) in
+ if dom = [] then str "[]" else
+ str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+let ppidmapgen l = pp (pridmapgen l)
+
let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
hov 0
(Termops.print_constr (EConstr.of_constr c) ++
@@ -116,7 +122,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
and pr_closed_glob_constr_idmap x =
pridmap (fun _ -> pr_closed_glob_constr) x
and pr_closed_glob_constr {closure=closure;term=term} =
- pr_closure closure ++ pr_lglob_constr term
+ pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term
let ppclosure x = pp (pr_closure x)
let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
@@ -125,24 +131,24 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
let pP s = pp (hov 0 s)
let safe_pr_global = function
- | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")")
- | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
+ | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")")
+ | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
int i ++ str ")")
- | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
+ | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
int i ++ str "," ++ int j ++ str ")")
| VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")")
let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
let ppconst (sp,j) =
- pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val)
+ pp (str"#" ++ KerName.print sp ++ str"=" ++ envpp pr_lconstr_env j.uj_val)
let ppvar ((id,a)) =
- pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a)
+ pp (str"#" ++ Id.print id ++ str":" ++ envpp pr_lconstr_env a)
let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
-let ppj j = pp (genppj pr_ljudge j)
+let ppj j = pp (genppj (envpp pr_ljudge_env) j)
let prsubst s = pp (Mod_subst.debug_pr_subst s)
let prdelta s = pp (Mod_subst.debug_pr_delta s)
@@ -170,13 +176,13 @@ let ppclenv clenv = pp(pr_clenv clenv)
let ppgoalgoal gl = pp(Goal.pr_goal gl)
let ppgoal g = pp(Printer.pr_goal g)
let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g))
-let pphintdb db = pp(Hints.pr_hint_db db)
+let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
let ppproofview p =
let gls,sigma = Proofview.proofview p in
pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
let ppopenconstr (x : Evd.open_constr) =
- let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c)
+ let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c)
(* spiwack: deactivated until a replacement is found
let pppftreestate p = pp(print_pftreestate p)
*)
@@ -226,7 +232,7 @@ let ppenv e = pp
let ppenvwithcst e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
- str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+ str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x))
@@ -242,7 +248,7 @@ let cast_kind_display k =
| NATIVEcast -> "NATIVEcast"
let constr_display csr =
- let rec term_display c = match kind_of_term c with
+ let rec term_display c = match kind c with
| Rel n -> "Rel("^(string_of_int n)^")"
| Meta n -> "Meta("^(string_of_int n)^")"
| Var id -> "Var("^(Id.to_string id)^")"
@@ -258,13 +264,13 @@ let constr_display csr =
^(term_display t)^","^(term_display c)^")"
| App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
| Evar (e,l) -> "Evar("^(string_of_existential e)^","^(array_display l)^")"
- | Const (c,u) -> "Const("^(string_of_con c)^","^(universes_display u)^")"
+ | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
| Ind ((sp,i),u) ->
- "MutInd("^(string_of_mind sp)^","^(string_of_int i)^","^(universes_display u)^")"
+ "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"
| Construct (((sp,i),j),u) ->
- "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
+ "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
^","^(universes_display u)^(string_of_int j)^")"
- | Proj (p, c) -> "Proj("^(string_of_con (Projection.constant p))^","^term_display c ^")"
+ | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
| Case (ci,p,c,bl) ->
"MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
^(array_display bl)^")"
@@ -314,7 +320,7 @@ let constr_display csr =
open Format;;
let print_pure_constr csr =
- let rec term_display c = match kind_of_term c with
+ let rec term_display c = match Constr.kind c with
| Rel n -> print_string "#"; print_int n
| Meta n -> print_string "Meta("; print_int n; print_string ")"
| Var id -> print_string (Id.to_string id)
@@ -432,7 +438,7 @@ let print_pure_constr csr =
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (debug_string_of_mind sp)
+ print_string (MutInd.debug_to_string sp)
and sp_con_display sp =
(* let dir,l = decode_kn sp in
let ls =
@@ -441,7 +447,7 @@ let print_pure_constr csr =
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (debug_string_of_con sp)
+ print_string (Constant.debug_to_string sp)
in
try
@@ -503,7 +509,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun _ -> in_current_context constr_display c)
+ (fun _ st -> in_current_context constr_display c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
@@ -519,7 +525,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun _ -> in_current_context print_pure_constr c)
+ (fun _ st -> in_current_context print_pure_constr c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index afa94a63e0..8e43bf6ed0 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -10,11 +10,11 @@ let ppripos (ri,pos) =
| Reloc_annot a ->
let sp,i = a.ci.ci_ind in
print_string
- ("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n")
+ ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->
- print_string ("getglob "^(string_of_con kn)^"\n"));
+ print_string ("getglob "^(Constant.to_string kn)^"\n"));
print_flush ()
let print_vfix () = print_string "vfix"
@@ -32,7 +32,7 @@ let print_idkey idk =
match idk with
| ConstKey sp ->
print_string "Cons(";
- print_string (string_of_con sp);
+ print_string (Constant.to_string sp);
print_string ")"
| VarKey id -> print_string (Id.to_string id)
| RelKey i -> print_string "~";print_int i
@@ -63,7 +63,7 @@ and ppatom a =
| Aid idk -> print_idkey idk
| Atype u -> print_string "Type(...)"
| Aind(sp,i) -> print_string "Ind(";
- print_string (string_of_mind sp);
+ print_string (MutInd.to_string sp);
print_string ","; print_int i;
print_string ")"
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-17 02:38:28 +0000