aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include4
-rw-r--r--dev/ci/ci-basic-overlay.sh12
-rwxr-xr-xdev/ci/ci-fiat-parsers.sh2
-rw-r--r--dev/ci/ci-user-overlay.sh18
-rw-r--r--dev/doc/changes.txt16
-rw-r--r--dev/tools/Makefile.devel2
-rw-r--r--dev/top_printers.ml36
-rw-r--r--dev/vm_printers.ml1
8 files changed, 60 insertions, 31 deletions
diff --git a/dev/base_include b/dev/base_include
index 608624d06e..defea713d8 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -18,10 +18,12 @@
#directory "intf";;
#directory "stm";;
#directory "vernac";;
+#directory "../API";;
#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
+#load "API.cma";;
#use "top_printers.ml";;
#use "vm_printers.ml";;
@@ -56,6 +58,8 @@
(* Open main files *)
+open API
+open Grammar_API
open Names
open Term
open Vars
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a6972c9500..7a9df93c45 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -85,8 +85,8 @@
########################################################################
# fiat_parsers
########################################################################
-: ${fiat_parsers_CI_BRANCH:=master}
-: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+: ${fiat_parsers_CI_BRANCH:=trunk__API}
+: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git}
########################################################################
# fiat_crypto
@@ -97,14 +97,14 @@
########################################################################
# bedrock_src
########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${bedrock_src_CI_BRANCH:=trunk__API}
+: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
########################################################################
# bedrock_facade
########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${bedrock_facade_CI_BRANCH:=trunk__API}
+: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
########################################################################
# formal-topology
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index c62aa1d859..2095245eb8 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
-( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples && make -j ${NJOBS} fiat-core )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index bfa43cde1d..0edaf07efc 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -25,10 +25,18 @@ echo $TRAVIS_PULL_REQUEST
echo $TRAVIS_BRANCH
echo $TRAVIS_COMMIT
-if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then
-
- mathcomp_CI_BRANCH=coqlib-part-02
- mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
-
+if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
+ mathcomp_CI_BRANCH=ssr-merge
+ mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
fi
+echo "DEBUG: ci-user-overlay.sh 0"
+if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
+ echo "DEBUG: ci-user-overlay.sh 1"
+ bedrock_src_CI_BRANCH=trunk__API
+ bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
+ bedrock_facade_CI_BRANCH=trunk__API
+ bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
+ fiat_parsers_CI_BRANCH=trunk__API
+ fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
+fi
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7fad65bf0a..bcda4ff50a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,6 +51,12 @@ In Constrexpr_ops:
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
ones were preserving the original sharing of the type.
+In Nameops:
+
+ The API has been made more uniform. New combinators added in the
+ "Name" space name. Function "out_name" now fails with IsAnonymous
+ rather than with Failure "Nameops.out_name".
+
Location handling and AST attributes:
Location handling has been reworked. First, Loc.ghost has been
@@ -113,13 +119,17 @@ In Coqlib / reference location:
We have removed from Coqlib functions returning `constr` from
names. Now it is only possible to obtain references, that must be
processed wrt the particular needs of the client.
+ We have changed in constrintern the functions returnin `constr` as
+ well to return global references instead.
Users of `coq_constant/gen_constant` can do
`Universes.constr_of_global (find_reference dir r)` _however_ note
the warnings in the `Universes.constr_of_global` in the
documentation. It is very likely that you were previously suffering
from problems with polymorphic universes due to using
- `Coqlib.coq_constant` that used to do this.
+ `Coqlib.coq_constant` that used to do this. You must rather use
+ `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
+ when constructing terms in ML (see univpoly.txt for more information).
** Tactic API **
@@ -127,6 +137,10 @@ In Coqlib / reference location:
Thus it only generates one instance of the global reference, and it is the
caller's responsibility to perform a focus on the goal.
+- pf_global, construct_reference, global_reference,
+ global_reference_in_absolute_module now return a global_reference
+ instead of a constr.
+
- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
was very specific. Use tclPROGRESS instead.
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
index 8dcc70cf7f..ffdb1bdca9 100644
--- a/dev/tools/Makefile.devel
+++ b/dev/tools/Makefile.devel
@@ -5,7 +5,7 @@
TOPDIR=.
BASEDIR=
-SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
+SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API
default: usage noargument
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 07a47c8b7a..6ae5125f6d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,6 +8,7 @@
(* Printers for the ocaml toplevel. *)
+open API
open Util
open Pp
open Names
@@ -36,7 +37,7 @@ let pp x = Pp.pp_with !Topfmt.std_ft x
let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
(* name printers *)
-let ppid id = pp (pr_id id)
+let ppid id = pp (Id.print id)
let pplab l = pp (pr_lab l)
let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
let ppdir dir = pp (pr_dirpath dir)
@@ -78,12 +79,12 @@ let ppbigint n = pp (str (Bigint.to_string n));;
let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Int.Set.elements l))
-let ppidset l = pp (prset pr_id (Id.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
let pridmap pr l =
- let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in
+ 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)
@@ -94,10 +95,10 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
(match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
Termops.print_constr (EConstr.of_constr c) ++ str">") ++
(if id = id0 then mt ()
- else spc () ++ str "<canonical: " ++ pr_id id ++ str ">"))))
+ else spc () ++ str "<canonical: " ++ Id.print id ++ str ">"))))
-let prididmap = pridmap (fun _ -> pr_id)
-let ppididmap = ppidmap (fun _ -> pr_id)
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]")
@@ -131,15 +132,15 @@ let safe_pr_global = function
int i ++ str ")")
| ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
int i ++ str "," ++ int j ++ str ")")
- | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ 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"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val)
+ pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val)
let ppvar ((id,a)) =
- pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a)
+ pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a)
let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
@@ -492,6 +493,7 @@ VERNAC COMMAND EXTEND PrintConstr
END
*)
+open Grammar_API
open Genarg
open Stdarg
open Egramml
@@ -536,21 +538,21 @@ let encode_path ?loc prefix mpdir suffix id =
let dir = match mpdir with
| None -> []
| Some (mp,dir) ->
- (DirPath.repr (dirpath_of_string (string_of_mp mp))@
+ (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
DirPath.repr dir) in
Qualid (Loc.tag ?loc @@ make_qualid
(DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
let raw_string_of_ref ?loc _ = function
| ConstRef cst ->
- let (mp,dir,id) = repr_con cst in
+ let (mp,dir,id) = Constant.repr3 cst in
encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id)
| IndRef (kn,i) ->
- let (mp,dir,id) = repr_mind kn in
+ let (mp,dir,id) = MutInd.repr3 kn in
encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id]
(Id.of_string ("_"^string_of_int i))
| ConstructRef ((kn,i),j) ->
- let (mp,dir,id) = repr_mind kn in
+ let (mp,dir,id) = MutInd.repr3 kn in
encode_path ?loc "CSTR" (Some (mp,dir))
[Label.to_id id;Id.of_string ("_"^string_of_int i)]
(Id.of_string ("_"^string_of_int j))
@@ -559,14 +561,14 @@ let raw_string_of_ref ?loc _ = function
let short_string_of_ref ?loc _ = function
| VarRef id -> Ident (Loc.tag ?loc id)
- | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_con cst)))
- | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_mind kn)))
+ | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst)))
+ | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn)))
| IndRef (kn,i) ->
- encode_path ?loc "IND" None [Label.to_id (pi3 (repr_mind kn))]
+ encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
(Id.of_string ("_"^string_of_int i))
| ConstructRef ((kn,i),j) ->
encode_path ?loc "CSTR" None
- [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)]
+ [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)]
(Id.of_string ("_"^string_of_int j))
(* Anticipate that printers can be used from ocamldebug and that
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index afa94a63e0..be6b914b6b 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,3 +1,4 @@
+open API
open Format
open Term
open Names
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:06:51 +0000