diff options
112 files changed, 1201 insertions, 843 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3a626796a6..c3e59a6d89 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -62,6 +62,7 @@ before_script: # TODO figure out how to build doc for installed Coq .build-template: stage: stage-1 + interruptible: true artifacts: name: "$CI_JOB_NAME" paths: @@ -98,6 +99,7 @@ before_script: # Template for building Coq + stdlib, typical use: overload the switch .dune-template: stage: stage-1 + interruptible: true dependencies: [] script: - set -e @@ -117,6 +119,7 @@ before_script: .dune-ci-template: stage: stage-2 + interruptible: true needs: - build:edge+flambda:dune:dev dependencies: @@ -143,6 +146,7 @@ before_script: .doc-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -158,6 +162,7 @@ before_script: # set dependencies when using .test-suite-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -179,6 +184,7 @@ before_script: # set dependencies when using .validate-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -195,6 +201,7 @@ before_script: .ci-template: stage: stage-2 + interruptible: true script: - set -e - echo 'start:coq.test' @@ -218,6 +225,7 @@ before_script: .windows-template: stage: stage-1 + interruptible: true artifacts: name: "%CI_JOB_NAME%" paths: @@ -226,7 +234,7 @@ before_script: expire_in: 1 week dependencies: [] tags: - - windows + - windows-inria before_script: [] script: - call dev/ci/gitlab.bat @@ -320,6 +328,7 @@ lint: pkg:opam: stage: stage-1 + interruptible: true # OPAM will build out-of-tree so no point in importing artifacts dependencies: [] script: @@ -336,6 +345,7 @@ pkg:opam: .nix-template: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git + interruptible: true stage: stage-1 variables: # By default we use coq.cachix.org as an extra substituter but this can be overridden diff --git a/Makefile.doc b/Makefile.doc index 125a4b33d5..50c4acb416 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -129,6 +129,8 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst) # Standard library ###################################################################### +DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 + ### Standard library (browsable html format) ifdef QUICK @@ -139,7 +141,7 @@ endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ - -R theories Coq -R plugins Coq $(VFILES) + $(DOCLIBS) $(VFILES) mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index @@ -178,12 +180,12 @@ doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp endif diff --git a/Makefile.dune b/Makefile.dune index bafb40d55f..b433ed1b94 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -6,7 +6,7 @@ .PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accessory targets -.PHONY: ocheck ireport clean # Maintenance targets +.PHONY: fmt ocheck ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -36,6 +36,7 @@ help: @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @echo "" + @echo " - fmt: run ocamlformat on the codebase" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @@ -100,6 +101,9 @@ apidoc: voboot release: voboot dune build $(DUNEOPT) -p coq +fmt: voboot + dune build @fmt + ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all diff --git a/checker/check.ml b/checker/check.ml index ffb2928d55..4ac5c56732 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -294,14 +294,22 @@ type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = depe (* Dependency graph *) let depgraph = ref LibraryMap.empty -let marshal_in_segment f ch = - try - let stop = input_binary_int ch in - let v = Analyze.instantiate (Analyze.parse_channel ch) in - let digest = Digest.input ch in +let marshal_in_segment ~validate ~value f ch = + if validate then + let v, stop, digest = + try + let stop = input_binary_int ch in + let v = Analyze.parse_channel ch in + let digest = Digest.input ch in + v, stop, digest + with _ -> + user_err (str "Corrupted file " ++ quote (str f)) + in + let () = Validate.validate ~debug:!Flags.debug value v in + let v = Analyze.instantiate v in Obj.obj v, stop, digest - with _ -> - user_err (str "Corrupted file " ++ quote (str f)) + else + System.marshal_in_segment f ch let skip_in_segment f ch = try @@ -312,30 +320,26 @@ let skip_in_segment f ch = with _ -> user_err (str "Corrupted file " ++ quote (str f)) -let marshal_or_skip ~intern_mode f ch = - if intern_mode <> Dep then - let v, pos, digest = marshal_in_segment f ch in +let marshal_or_skip ~validate ~value f ch = + if validate then + let v, pos, digest = marshal_in_segment ~validate ~value f ch in Some v, pos, digest else let pos, digest = skip_in_segment f ch in None, pos, digest let intern_from_file ~intern_mode (dir, f) = - let validate a b c = if intern_mode <> Dep then Validate.validate a b c in + let validate = intern_mode <> Dep in Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try - let marshal_in_segment f ch = if intern_mode <> Dep - then marshal_in_segment f ch - else System.marshal_in_segment f ch - in let ch = System.with_magic_number_check raw_intern_library f in - let (sd:summary_disk), _, digest = marshal_in_segment f ch in - let (md:library_disk), _, digest = marshal_in_segment f ch in - let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in - let (tasks:'a option), _, _ = marshal_in_segment f ch in + let (sd:summary_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_libsum f ch in + let (md:library_disk), _, digest = marshal_in_segment ~validate ~value:Values.v_lib f ch in + let (opaque_csts:seg_univ option), _, udg = marshal_in_segment ~validate ~value:Values.v_univopaques f ch in + let (tasks:'a option), _, _ = marshal_in_segment ~validate ~value:Values.(Opt Any) f ch in let (table:seg_proofs option), pos, checksum = - marshal_or_skip ~intern_mode f ch in + marshal_or_skip ~validate ~value:Values.v_opaquetable f ch in (* Verification of the final checksum *) let () = close_in ch in let ch = open_in_bin f in @@ -354,12 +358,7 @@ let intern_from_file ~intern_mode (dir, f) = user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; - validate !Flags.debug Values.v_univopaques opaque_csts; end; - (* Verification of the unmarshalled values *) - validate !Flags.debug Values.v_libsum sd; - validate !Flags.debug Values.v_lib md; - validate !Flags.debug Values.(Opt v_opaquetable) table; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = if opaque_csts <> None then Safe_typing.Dvivo (digest,udg) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 06ee4fcc7a..e606d60d96 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -73,7 +73,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) - | (RegularArity _ | TemplateArity _), _ -> false + | (RegularArity _ | TemplateArity _), _ -> assert false let check_kelim k1 k2 = Sorts.family_leq k1 k2 @@ -139,7 +139,7 @@ let check_inductive env mind mb = let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; - mind_universes; mind_variance; + mind_universes; mind_variance; mind_sec_variance; mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) @@ -148,7 +148,7 @@ let check_inductive env mind mb = check_positive = mb_flags.check_positive; check_universes = mb_flags.check_universes; conv_oracle = mb_flags.conv_oracle} env in - Indtypes.check_inductive env mind entry + Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in @@ -165,7 +165,9 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) - ignore mind_variance; (* Indtypes did the necessary checking *) + check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal) + mb.mind_variance mind_variance); + check "mind_sec_variance" (Option.is_empty mind_sec_variance); ignore mind_private; (* passed through Indtypes *) ignore mind_typing_flags; diff --git a/checker/validate.ml b/checker/validate.ml index 070a112bb6..6ffc43394b 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -8,32 +8,39 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Analyze + (* This module defines validation functions to ensure an imported value (using input_value) has the correct structure. *) -let rec pr_obj_rec o = - if Obj.is_int o then - Format.print_int(Obj.magic o) - else if Obj.is_block o then - let t = Obj.tag o in - if t > Obj.no_scan_tag then - if t = Obj.string_tag then - Format.print_string ("\""^String.escaped(Obj.magic o)^"\"") - else - Format.print_string "?" - else - (let n = Obj.size o in - Format.print_string ("#"^string_of_int t^"("); - Format.open_hvbox 0; - for i = 0 to n-1 do - pr_obj_rec (Obj.field o i); - if i<>n-1 then (Format.print_string ","; Format.print_cut()) - done; - Format.close_box(); - Format.print_string ")") - else Format.print_string "?" - -let pr_obj o = pr_obj_rec o; Format.print_newline() +let rec pr_obj_rec mem o = match o with +| Int i -> + Format.print_int i +| Ptr p -> + let v = LargeArray.get mem p in + begin match v with + | Struct (tag, data) -> + let n = Array.length data in + Format.print_string ("#"^string_of_int tag^"("); + Format.open_hvbox 0; + for i = 0 to n-1 do + pr_obj_rec mem (Array.get data i); + if i<>n-1 then (Format.print_string ","; Format.print_cut()) + done; + Format.close_box(); + Format.print_string ")" + | String s -> + Format.print_string ("\""^String.escaped s^"\"") + | Int64 _ + | Float64 _ -> + Format.print_string "?" + end +| Atm tag -> + Format.print_string ("#"^string_of_int tag^"()"); +| Fun addr -> + Format.printf "fun@%x" addr + +let pr_obj mem o = pr_obj_rec mem o; Format.print_newline() (**************************************************************************) (* Obj low-level validators *) @@ -48,63 +55,115 @@ type error_context = error_frame list let mt_ec : error_context = [] let (/) (ctx:error_context) s : error_context = s::ctx -exception ValidObjError of string * error_context * Obj.t -let fail ctx o s = raise (ValidObjError(s,ctx,o)) +exception ValidObjError of string * error_context * data +let fail _mem ctx o s = raise (ValidObjError(s,ctx,o)) + +let is_block mem o = match o with +| Ptr _ | Atm _ -> true +| Fun _ | Int _ -> false + +let is_int _mem o = match o with +| Int _ -> true +| Fun _ | Ptr _ | Atm _ -> false + +let is_int64 mem o = match o with +| Int _ | Fun _ | Atm _ -> false +| Ptr p -> + match LargeArray.get mem p with + | Int64 _ -> true + | Float64 _ | Struct _ | String _ -> false + +let is_float64 mem o = match o with +| Int _ | Fun _ | Atm _ -> false +| Ptr p -> + match LargeArray.get mem p with + | Float64 _ -> true + | Int64 _ | Struct _ | String _ -> false + +let get_int _mem = function +| Int i -> i +| Fun _ | Ptr _ | Atm _ -> assert false + +let tag mem o = match o with +| Atm tag -> tag +| Fun _ -> Obj.out_of_heap_tag +| Int _ -> Obj.int_tag +| Ptr p -> + match LargeArray.get mem p with + | Struct (tag, _) -> tag + | String _ -> Obj.string_tag + | Float64 _ -> Obj.double_tag + | Int64 _ -> Obj.custom_tag + +let size mem o = match o with +| Atm _ -> 0 +| Fun _ | Int _ -> assert false +| Ptr p -> + match LargeArray.get mem p with + | Struct (tag, blk) -> Array.length blk + | String _ | Float64 _ | Int64 _ -> assert false + +let field mem o i = match o with +| Atm _ | Fun _ | Int _ -> assert false +| Ptr p -> + match LargeArray.get mem p with + | Struct (tag, blk) -> Array.get blk i + | String _ | Float64 _ | Int64 _ -> assert false (* Check that object o is a block with tag t *) -let val_tag t ctx o = - if Obj.is_block o && Obj.tag o = t then () - else fail ctx o ("expected tag "^string_of_int t) - -let val_block ctx o = - if Obj.is_block o then - (if Obj.tag o > Obj.no_scan_tag then - fail ctx o "block: found no scan tag") - else fail ctx o "expected block obj" - -let val_dyn ctx o = - let fail () = fail ctx o "expected a Dyn.t" in - if not (Obj.is_block o) then fail () - else if not (Obj.size o = 2) then fail () - else if not (Obj.tag (Obj.field o 0) = Obj.int_tag) then fail () +let val_tag t mem ctx o = + if is_block mem o && tag mem o = t then () + else fail mem ctx o ("expected tag "^string_of_int t) + +let val_block mem ctx o = + if is_block mem o then + (if tag mem o > Obj.no_scan_tag then + fail mem ctx o "block: found no scan tag") + else fail mem ctx o "expected block obj" + +let val_dyn mem ctx o = + let fail () = fail mem ctx o "expected a Dyn.t" in + if not (is_block mem o) then fail () + else if not (size mem o = 2) then fail () + else if not (tag mem (field mem o 0) = Obj.int_tag) then fail () else () open Values -let rec val_gen v ctx o = match v with - | Tuple (name,vs) -> val_tuple ~name vs ctx o - | Sum (name,cc,vv) -> val_sum name cc vv ctx o - | Array v -> val_array v ctx o - | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] ctx o - | Opt v -> val_sum "option" 1 [|[|v|]|] ctx o - | Int -> if not (Obj.is_int o) then fail ctx o "expected an int" +let rec val_gen v mem ctx o = match v with + | Tuple (name,vs) -> val_tuple ~name vs mem ctx o + | Sum (name,cc,vv) -> val_sum name cc vv mem ctx o + | Array v -> val_array v mem ctx o + | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] mem ctx o + | Opt v -> val_sum "option" 1 [|[|v|]|] mem ctx o + | Int -> if not (is_int mem o) then fail mem ctx o "expected an int" | String -> - (try val_tag Obj.string_tag ctx o - with Failure _ -> fail ctx o "expected a string") + (try val_tag Obj.string_tag mem ctx o + with Failure _ -> fail mem ctx o "expected a string") | Any -> () - | Fail s -> fail ctx o ("unexpected object " ^ s) - | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o - | Dyn -> val_dyn ctx o - | Proxy { contents = v } -> val_gen v ctx o - | Uint63 -> val_uint63 ctx o - | Float64 -> val_float64 ctx o + | Fail s -> fail mem ctx o ("unexpected object " ^ s) + | Annot (s,v) -> val_gen v mem (ctx/CtxAnnot s) o + | Dyn -> val_dyn mem ctx o + | Proxy { contents = v } -> val_gen v mem ctx o + | Int64 -> val_int64 mem ctx o + | Float64 -> val_float64 mem ctx o (* Check that an object is a tuple (or a record). vs is an array of value representation for each field. Its size corresponds to the expected size of the object. *) -and val_tuple ?name vs ctx o = +and val_tuple ?name vs mem ctx o = let ctx = match name with | Some n -> ctx/CtxType n | _ -> ctx in let n = Array.length vs in let val_fld i v = - val_gen v (ctx/(CtxField i)) (Obj.field o i) in - val_block ctx o; - if Obj.size o = n then Array.iteri val_fld vs + val_gen v mem (ctx/(CtxField i)) (field mem o i) in + val_block mem ctx o; + if size mem o = n then Array.iteri val_fld vs else - fail ctx o - ("tuple size: found "^string_of_int (Obj.size o)^ + fail mem ctx o + ("tuple size: found "^string_of_int (size mem o)^ ", expected "^string_of_int n) (* Check that the object is either a constant constructor of tag < cc, @@ -113,35 +172,35 @@ and val_tuple ?name vs ctx o = The size of vv corresponds to the number of non-constant constructors, and the size of vv.(i) is the expected arity of the i-th non-constant constructor. *) -and val_sum name cc vv ctx o = +and val_sum name cc vv mem ctx o = let ctx = ctx/CtxType name in - if Obj.is_block o then - (val_block ctx o; + if is_block mem o then + (val_block mem ctx o; let n = Array.length vv in - let i = Obj.tag o in + let i = tag mem o in let ctx' = if n=1 then ctx else ctx/CtxTag i in - if i < n then val_tuple vv.(i) ctx' o - else fail ctx' o ("sum: unexpected tag")) - else if Obj.is_int o then - let (n:int) = Obj.magic o in + if i < n then val_tuple vv.(i) mem ctx' o + else fail mem ctx' o ("sum: unexpected tag")) + else if is_int mem o then + let (n:int) = get_int mem o in (if n<0 || n>=cc then - fail ctx o ("bad constant constructor "^string_of_int n)) - else fail ctx o "not a sum" + fail mem ctx o ("bad constant constructor "^string_of_int n)) + else fail mem ctx o "not a sum" (* Check the o is an array of values satisfying f. *) -and val_array v ctx o = - val_block (ctx/CtxType "array") o; - for i = 0 to Obj.size o - 1 do - val_gen v ctx (Obj.field o i) +and val_array v mem ctx o = + val_block mem (ctx/CtxType "array") o; + for i = 0 to size mem o - 1 do + val_gen v mem ctx (field mem o i) done -and val_uint63 ctx o = - if not (Uint63.is_uint63 o) then - fail ctx o "not a 63-bit unsigned integer" +and val_int64 mem ctx o = + if not (is_int64 mem o) then + fail mem ctx o "not a 63-bit unsigned integer" -and val_float64 ctx o = - if not (Float64.is_float64 o) then - fail ctx o "not a 64-bit float" +and val_float64 mem ctx o = + if not (is_float64 mem o) then + fail mem ctx o "not a 64-bit float" let print_frame = function | CtxType t -> t @@ -149,12 +208,11 @@ let print_frame = function | CtxField i -> Printf.sprintf "fld=%i" i | CtxTag i -> Printf.sprintf "tag=%i" i -let validate debug v x = - let o = Obj.repr x in - try val_gen v mt_ec o +let validate ~debug v (o, mem) = + try val_gen v mem mt_ec o with ValidObjError(msg,ctx,obj) -> (if debug then let ctx = List.rev_map print_frame ctx in print_endline ("Context: "^String.concat"/"ctx); - pr_obj obj); + pr_obj mem obj); failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")") diff --git a/checker/validate.mli b/checker/validate.mli index fbcea3121b..584ea6ed95 100644 --- a/checker/validate.mli +++ b/checker/validate.mli @@ -8,4 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val validate : bool -> Values.value -> 'a -> unit +open Analyze + +val validate : debug:bool -> Values.value -> data * obj LargeArray.t -> unit diff --git a/checker/values.ml b/checker/values.ml index 56321a27ff..fff166f27b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -34,7 +34,7 @@ type value = | Dyn | Proxy of value ref - | Uint63 + | Int64 | Float64 let fix (f : value -> value) : value = @@ -129,6 +129,9 @@ let v_cast = v_enum "cast_kind" 4 let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|] let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] +let v_uint63 = + if Sys.word_size == 64 then Int else Int64 + let rec v_constr = Sum ("constr",0,[| [|Int|]; (* Rel *) @@ -148,7 +151,7 @@ let rec v_constr = [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) - [|Uint63|]; (* Int *) + [|v_uint63|]; (* Int *) [|Float64|] (* Int *) |]) @@ -299,6 +302,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_univs; (* universes *) Opt (Array v_variance); + Opt (Array v_variance); Opt v_bool; v_typing_flags|] diff --git a/checker/values.mli b/checker/values.mli index ec3b91d5dd..15d307ee29 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -38,7 +38,7 @@ type value = | Proxy of value ref (** Same as the inner value, used to define recursive types *) - | Uint63 + | Int64 | Float64 (** NB: List and Opt have their own constructors to make it easy to diff --git a/checker/votour.ml b/checker/votour.ml index 9adcc874ac..452809f7bb 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -157,7 +157,7 @@ let rec get_name ?(extra=false) = function |Annot (s,v) -> s^"/"^get_name ~extra v |Dyn -> "<dynamic>" | Proxy v -> get_name ~extra !v - | Uint63 -> "Uint63" + | Int64 -> "Int64" | Float64 -> "Float64" (** For tuples, its quite handy to display the inner 1st string (if any). @@ -263,7 +263,7 @@ let rec get_children v o pos = match v with end |Fail s -> raise Forbidden | Proxy v -> get_children !v o pos - | Uint63 -> raise Exit + | Int64 -> raise Exit | Float64 -> raise Exit let get_children v o pos = @@ -29,7 +29,6 @@ depends: [ build: [ [ "./configure" "-prefix" prefix "-native-compiler" "no" ] - [ "dune" "build" "@vodeps" ] - [ "dune" "exec" "coq_dune" "_build/default/.vfiles.d" ] + [ "make" "-f" "Makefile.dune" "voboot" ] [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index c75acb0560..577ce35aae 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -420,6 +420,7 @@ copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOT ECHO ========== BUILD COQ ==========
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+RMDIR /S /Q "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index f04de0ce6c..9e9e3b4cfa 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -97,8 +97,11 @@ ######################################################################## # Coquelicot ######################################################################## -: "${coquelicot_CI_REF:=master}" -: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" +# Modified until https://gitlab.inria.fr/coquelicot/coquelicot/merge_requests/2 is merged +: "${coquelicot_CI_REF:=fix-rlist-import}" +: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/pedrot/coquelicot}" +# : "${coquelicot_CI_REF:=master}" +# : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" ######################################################################## diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 2b1d2298f2..b9d6215e60 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -4,7 +4,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2 -data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) + +# "latest" is disabled due to lack of build credits upstream, thus artifacts fail +# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) +data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -) mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh new file mode 100644 index 0000000000..a125337dd9 --- /dev/null +++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh @@ -0,0 +1,33 @@ +if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then + + mathcomp_CI_REF=non_maximal_implicit + mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp + + oddorder_CI_REF=non_maximal_implicit + oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order + + stdlib2_CI_REF=non_maximal_implicit + stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2 + + coq_dpdgraph_CI_REF=non_maximal_implicit + coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph + + vst_CI_REF=non_maximal_implicit + vst_CI_GITURL=https://github.com/SimonBoulier/VST + + equations_CI_REF=non_maximal_implicit + equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations + + mtac2_CI_REF=non_maximal_implicit + mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2 + + relation_algebra_CI_REF=non_maximal_implicit + relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra + + fiat_parsers_CI_REF=non_maximal_implicit + fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat + + Corn_CI_REF=non_maximal_implicit + Corn_CI_GITURL=https://github.com/SimonBoulier/corn + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 37c6e2f619..cd35064b18 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,24 +108,44 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec -- dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg coqc foo.v (ocd) source dune_db ``` -or +to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`: ``` -dune exec -- dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker foo.vo (ocd) source 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. +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. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. +**Note**: If you are using OCaml >= 4.08 you need to use + +``` +(ocd) source dune_db_408 +``` + +or + +``` +(ocd) source dune_db_409 +``` + +depending on your OCaml version. This is due to several factors: + +- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source` + is not re entrant and seems to doubly-load in the default setup, see + https://github.com/coq/coq/issues/8952 +- OCaml >= 4.09 comes with `dynlink` already linked in so we need to + modify the list of modules loaded. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 2d187f7bae..3260040248 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -158,7 +158,7 @@ Universes component: universe polymorphism, asynchronous proofs summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one - impacted released: V8.5-V8.10 + impacted released versions: V8.5-V8.10 impacted development branches: none impacted coqchk versions: immune fixed in: PR#10664 @@ -167,6 +167,19 @@ Universes GH issue number: none risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + component: algebraic universes + summary: Set+2 was incorrectly simplified to Set+1 + introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a) + impacted released versions: V8.10.0 V8.10.1 V8.10.2 + impacted coqchk versions: same + fixed in: PR#11422 + found by: Gilbert + exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration) + GH issue number: see PR + risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic + universes such that +2 increments do not appear), mild risk from plugins which manipulate + algebraic universes. + Primitive projections component: primitive projections, guard condition diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 1c486b024d..ba68501e04 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -75,7 +75,8 @@ in time. - [ ] Pin the versions of libraries and plugins in `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it exists, a branch dedicated to compatibility with the corresponding - Coq branch). + Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this + semi-automatically. - [ ] Remove all remaining unmerged feature PRs from the beta milestone. - [ ] Start a new project to track PR backporting. The project should have a "Request X.X+beta1 inclusion" column for the PRs that were diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 0fc0a413ba..fca7b77fc2 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -1,12 +1,11 @@ # Coq XML Protocol This document is based on documentation originally written by CJ Bell -for his [vscoq](https://github.com/siegebell/vscoq/) project. +for his [vscoq](https://github.com/coq-community/vscoq/) project. Here, the aim is to provide a "hands on" description of the XML protocol that coqtop and IDEs use to communicate. The protocol first appeared -with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming -versions of Proof General. +with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). @@ -13,6 +13,8 @@ ../checker/coqchk.bc ../topbin/coqc_bin.bc ../ide/coqide_main.bc - ; This is not enough as the call to `ocamlfind` will fail :/ + %{lib:coq.plugins.ltac:ltac_plugin.cma} + ; This is not enough, the call to `ocamlfind` may fail if the + ; META file is not yet in place :/ top_printers.cma) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 1382f4d1b6..498f167eb1 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -7,11 +7,21 @@ case $1 in exe=_build/default/checker/coqchk.bc ;; coqide) + shift exe=_build/default/ide/coqide_main.bc ;; - *) + coqc) + shift exe=_build/default/topbin/coqc_bin.bc ;; + coqtop) + shift + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; + *) + echo "First argument must be one of {coqc,coqtop,checker,coqide}" + exit 1 + ;; esac emacs="${INSIDE_EMACS:+-emacs}" diff --git a/dev/dune_db_408 b/dev/dune_db_408 new file mode 100644 index 0000000000..3bf13da62d --- /dev/null +++ b/dev/dune_db_408 @@ -0,0 +1,25 @@ +load_printer threads.cma +load_printer str.cma +load_printer config.cma +load_printer clib.cma +load_printer dynlink.cma +load_printer lib.cma +load_printer gramlib.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 + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/dune_db_409 b/dev/dune_db_409 new file mode 100644 index 0000000000..1267fd5393 --- /dev/null +++ b/dev/dune_db_409 @@ -0,0 +1,24 @@ +load_printer threads.cma +load_printer str.cma +load_printer config.cma +load_printer clib.cma +load_printer lib.cma +load_printer gramlib.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 + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 224601bbce..553696410c 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -33,6 +33,6 @@ echo Checking overlays dev/tools/check-overlays.sh || CODE=1 echo Checking ocamlformat -dune build @fmt || CODE=1 +make -f Makefile.dune fmt || CODE=1 exit $CODE diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh new file mode 100755 index 0000000000..dbf54d7f0a --- /dev/null +++ b/dev/tools/pin-ci.sh @@ -0,0 +1,46 @@ +#!/usr/bin/env bash + +# Use this script to pin the commit used by the developments tracked by the CI + +OVERLAYS="./dev/ci/ci-basic-overlay.sh" + +process_development() { + local DEV=$1 + local REPO_VAR="${DEV}_CI_GITURL" + local REPO=${!REPO_VAR} + local BRANCH_VAR="${DEV}_CI_REF" + local BRANCH=${!BRANCH_VAR} + if [[ -z "$BRANCH" ]] + then + echo "$DEV has no branch set, skipping" + return 0 + fi + if [[ $BRANCH =~ ^[a-f0-9]{40}$ ]] + then + echo "$DEV is already set to hash $BRANCH, skipping" + return 0 + fi + echo "Resolving $DEV as $BRANCH from $REPO" + local HASH=$(git ls-remote --heads $REPO $BRANCH | cut -f 1) + if [[ -z "$HASH" ]] + then + echo "Could not resolve reference $BRANCH for $DEV (something went wrong), skipping" + return 0 + fi + read -p "Expand $DEV from $BRANCH to $HASH? [y/N] " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]]; then + # use -i.bak to be compatible with MacOS; see, e.g., https://stackoverflow.com/a/7573438/377022 + sed -i.bak -e "s/$BRANCH_VAR:=$BRANCH/$BRANCH_VAR:=$HASH/" $OVERLAYS + fi +} + +# Execute the script to set the overlay variables +. $OVERLAYS + +# Find all variables declared in the base overlay of the form *_CI_GITURL +for REPO_VAR in $(compgen -A variable | grep _CI_GITURL) +do + DEV=${REPO_VAR%_CI_GITURL} + process_development $DEV +done diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst deleted file mode 100644 index b3e3a78b96..0000000000 --- a/doc/changelog/01-kernel/11081-native-cleanup.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** the native compilation (:tacn:`native_compute`) now - creates a directory to contain temporary files instead of putting - them in the root of the system temporary directory. (`#11081 - <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst deleted file mode 100644 index 8c84648aa7..0000000000 --- a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** `#11360 <https://github.com/issues/11360>`_ - Broken section closing when a template polymorphic inductive type depends on - a section variable through its parameters (`#11361 - <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst deleted file mode 100644 index 8983e162fb..0000000000 --- a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Changed heuristics for universe minimization to :g:`Set`: only - minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, - by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst deleted file mode 100644 index 941469d698..0000000000 --- a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - A dependency was missing when looking for default clauses in the - algorithm for printing pattern matching clauses (`#11233 - <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing - `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry - Jay). diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst new file mode 100644 index 0000000000..a7ffde31fc --- /dev/null +++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst @@ -0,0 +1,6 @@ +- **Changed:** + The warning raised when a trailing implicit is declared to be non maximally + inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error. + This was deprecated since Coq 8.10. + (`#11368 <https://github.com/coq/coq/pull/11368>`_, + by SimonBoulier). diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst deleted file mode 100644 index a1b8594f5f..0000000000 --- a/doc/changelog/03-notations/11276-master+fix10750.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - :cmd:`Print Visibility` was failing in the presence of only-printing notations - (`#11276 <https://github.com/coq/coq/pull/11276>`_, - by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst deleted file mode 100644 index ae9888512d..0000000000 --- a/doc/changelog/03-notations/11311-custom-entries-recursive.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Recursive notations with custom entries were incorrectly parsing `constr` - instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ - by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, - `#9490 <https://github.com/coq/coq/pull/9490>`_). diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst deleted file mode 100644 index 2fef75dc7f..0000000000 --- a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The tactics :tacn:`eapply`, :tacn:`refine` and its variants no - longer allows shelved goals to be solved by typeclass resolution. - (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst new file mode 100644 index 0000000000..2afa3990ac --- /dev/null +++ b/doc/changelog/04-tactics/11023-nativecompute-timing.rst @@ -0,0 +1,7 @@ +- The :flag:`NativeCompute Timing` flag causes calls to + :tacn:`native_compute` (as well as kernel calls to the native + compiler) to emit separate timing information about compilation, + execution, and reification. It replaces the timing information + previously emitted when the `-debug` flag was set, and allows more + fine-grained timing of the native compiler. (`#11023 + <https://github.com/coq/coq/pull/11023>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst deleted file mode 100644 index cdfd2b228e..0000000000 --- a/doc/changelog/04-tactics/11203-fix-time-printing.rst +++ /dev/null @@ -1,4 +0,0 @@ -- The optional string argument to :tacn:`time` is now properly quoted - under :cmd:`Print Ltac` (`#11203 - <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 - <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst deleted file mode 100644 index ebfb6c19b1..0000000000 --- a/doc/changelog/04-tactics/11263-micromega-fix.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed** - Efficiency regression introduced by PR `#9725 <https://github.com/coq/coq/pull/9725>`_. - (`#11263 <https://github.com/coq/coq/pull/11263>`_, - fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, - and `#11242 <https://github.com/coq/coq/issues/11242>`_, - and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst deleted file mode 100644 index 25e929e030..0000000000 --- a/doc/changelog/04-tactics/11337-omega-with-depr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - The undocumented ``omega with`` tactic variant has been deprecated, - using ``lia`` is the recommended replacement, tho the old semantics - of ``omega with *`` can be recovered with ``zify; omega`` - (`#11337 <https://github.com/coq/coq/pull/11337>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst new file mode 100644 index 0000000000..5ecd46bced --- /dev/null +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Regression of ``lia`` due to more powerful ``zify`` + (`#11362 <https://github.com/coq/coq/pull/11362>`_, + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, + by Frédéric Besson). diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst deleted file mode 100644 index 462ba4a7b1..0000000000 --- a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. - (`#11241 <https://github.com/coq/coq/pull/11241>`_, - by Hugo Herbelin). diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst deleted file mode 100644 index ecc134748d..0000000000 --- a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coqtop --version`` was broken when called in the middle of an installation process - (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing - `#11254 <https://github.com/coq/coq/pull/11254>`_). diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst deleted file mode 100644 index 97f456036d..0000000000 --- a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated. - (`#11280 <https://github.com/coq/coq/pull/11280>`_, - by charguer). diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst deleted file mode 100644 index 599db5b1da..0000000000 --- a/doc/changelog/08-tools/11357-master.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable - together with an unpacked (``mllib``) plugin. (`#11357 - <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst deleted file mode 100644 index 10952c6b2c..0000000000 --- a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints - commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, - fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, - by Karl Palmskog). diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst new file mode 100644 index 0000000000..cb92945b8b --- /dev/null +++ b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Revert all buffers" command from CoqIDE which had been broken for a long time + (`#11415 <https://github.com/coq/coq/pull/11415>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst deleted file mode 100644 index 5c08e2b0ea..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` - environment variable - (`#11227 <https://github.com/coq/coq/pull/11227>`_, - by Bernhard M. Wiedemann). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7adb25cbd6..f9cc25959c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -529,8 +529,8 @@ sections, except in the following ways: Polymorphic Universe i. Fail Constraint i = i. - This includes constraints implictly declared by commands such as - :cmd:`Variable`, which may as a such need to be used with universe + This includes constraints implicitly declared by commands such as + :cmd:`Variable`, which may need to be used with universe polymorphism activated (locally by attribute or globally by option): .. coqtop:: all diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 21000889d3..6d9979a704 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -55,23 +55,23 @@ this version of Coq, it should soon be the case and we already recommend users to switch to :tacn:`lia` in new proof scripts (see also the warning message in the :ref:`corresponding chapter <omega>`). -The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| -and affected releases. See the `Changes in 8.11+beta1`_ section for the -detailed list of changes, including potentially breaking changes marked with -**Changed**. +The ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ +section and following sections for the detailed list of changes, +including potentially breaking changes marked with **Changed**. + +Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of +the ML API), https://coq.github.io/doc/v8.11/refman (reference +manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of +the standard library). Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the +Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of -the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference -manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of -the standard library). - The OPAM repository for |Coq| packages has been maintained by -Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions -from many users. A list of packages is available at +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with +contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. The 61 contributors to this version are Michael D. Adams, Guillaume @@ -514,6 +514,133 @@ Changes in 8.11+beta1 (`#10471 <https://github.com/coq/coq/pull/10471>`_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). +- **Fixed:** `#11360 <https://github.com/issues/11360>`_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). +- **Fixed:** The type of :g:`Set+1` would be computed to be itself, + leading to a proof of False (`#11422 + <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, + by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing + `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 <https://github.com/coq/coq/pull/11276>`_, + by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ + by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, + `#9490 <https://github.com/coq/coq/pull/9490>`_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) +- **Fixed:** + Efficiency regression of :tacn:`lia` introduced in 8.10 + by PR `#9725 <https://github.com/coq/coq/pull/9725>`_ + (`#11263 <https://github.com/coq/coq/pull/11263>`_, + fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, + and `#11242 <https://github.com/coq/coq/issues/11242>`_, + and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated. + Using :tacn:`lia` is the recommended replacement, though the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 <https://github.com/coq/coq/pull/11337>`_, + by Emilio Jesus Gallego Arias). +- **Fixed** + For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. + It can be enabled by explicitly loading the module :g:`ZifyPow` + (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 + (`#11241 <https://github.com/coq/coq/pull/11241>`_, + by Hugo Herbelin). + +**Commands and options** + +- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command + line options have been deprecated; their use was very limited, you + can achieve the same by adding object files in the linking step or + by using a plugin (`#11428 + <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego + Arias). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). +- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for + consistency with the new ``-vos`` and ``-vok`` flags. Usage of + ``-quick`` is now deprecated (`#11280 + <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin (`#11357 + <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). + +**CoqIDE** + +- **Changed:** CoqIDE now uses the GtkSourceView native implementation + of the autocomplete mechanism (`#11400 + <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot). + +**Standard library** + +- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and + :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be + imported explicitly where required (`#11396 + <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overridden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index bdfdffeaad..510e271951 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1728,11 +1728,11 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. warn:: Argument number @num is a trailing implicit so must be maximal. +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance in - .. coqtop:: all warn + .. coqtop:: all fail Arguments prod _ [_]. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 53cfb973d4..36a5916868 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3113,6 +3113,12 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the compilation, execution, and + reification phases of native compilation. + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this flag makes diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 7fe2493fbf..828caecabc 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,8 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins)) + (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} ; On windows run will fail @@ -17,6 +18,7 @@ ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. @@ -24,7 +26,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index ac611926b3..5e13214a1a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p> plugins/ssr/ssrfun.v </dd> + <dt> <b>Ltac2</b>: + The Ltac2 tactic programming language + </dt> + <dd> + user-contrib/Ltac2/Ltac2.v + user-contrib/Ltac2/Array.v + user-contrib/Ltac2/Bool.v + user-contrib/Ltac2/Char.v + user-contrib/Ltac2/Constr.v + user-contrib/Ltac2/Control.v + user-contrib/Ltac2/Env.v + user-contrib/Ltac2/Fresh.v + user-contrib/Ltac2/Ident.v + user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Int.v + user-contrib/Ltac2/List.v + user-contrib/Ltac2/Ltac1.v + user-contrib/Ltac2/Message.v + user-contrib/Ltac2/Notations.v + user-contrib/Ltac2/Option.v + user-contrib/Ltac2/Pattern.v + user-contrib/Ltac2/Std.v + user-contrib/Ltac2/String.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index bea6f24098..732f15b78a 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash # Instantiate links to library files in index template @@ -8,9 +8,14 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do + if [[ $k =~ "user-contrib" ]]; then + BASE_PREFIX="" + else + BASE_PREFIX="Coq." + fi d=`basename $k` ls $k | grep -q \.v'$' if [ $? = 0 ]; then @@ -26,7 +31,7 @@ for k in $LIBDIRS; do echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` - sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else diff --git a/engine/evd.ml b/engine/evd.ml index 8e7d942c37..70f58163fd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u = let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) -let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) +let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c) -let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i = + with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i) -let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) diff --git a/engine/evd.mli b/engine/evd.mli index 8843adc853..82e1003a65 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t -val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant -val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid + -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> Constant.t -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> GlobRef.t -> evar_map * econstr diff --git a/ide/coqide.ml b/ide/coqide.ml index 99a2ff0864..e0347d3c5f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -618,7 +618,7 @@ let printopts_callback opts v = let get_current_word term = (* First look to find if autocompleting *) - match term.script#complete_popup#proposal with + match term.script#proposal with | Some p -> p | None -> (* Then look at the current selected word *) @@ -996,8 +996,6 @@ let build_ui () = item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer"; item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w); item "Save all" ~label:"Sa_ve all" ~callback:File.saveall; - item "Revert all buffers" ~label:"_Revert all buffers" - ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED; item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE ~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer"; item "Print..." ~label:"_Print..." diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index f056af6703..59dd9c0e4c 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -36,7 +36,6 @@ let init () = \n <menuitem action='Save' />\ \n <menuitem action='Save as' />\ \n <menuitem action='Save all' />\ -\n <menuitem action='Revert all buffers' />\ \n <menuitem action='Close buffer' />\ \n <menuitem action='Print...' />\ \n <menu action='Export to'>\ diff --git a/ide/preferences.ml b/ide/preferences.ml index 4ee5669877..d3cf08e90e 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -388,6 +388,9 @@ let window_height = let auto_complete = new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool) +let auto_complete_delay = + new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int) + let stop_before = new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool) @@ -831,10 +834,26 @@ let configure ?(apply=(fun () -> ())) parent = let but = GButton.check_button ~label:text ~active ~packing:box#pack () in ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active)) in + let spin text ~min ~max (pref : int preference) = + let box = GPack.hbox ~packing:box#pack () in + let but = GEdit.spin_button + ~numeric:true ~update_policy:`IF_VALID ~digits:0 + ~packing:box#pack () + in + let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in + let () = but#adjustment#set_bounds + ~lower:(float_of_int min) ~upper:(float_of_int max) + ~step_incr:1. + () + in + let () = but#set_value (float_of_int pref#get) in + ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int)) + in let () = button "Dynamic word wrap" dynamic_word_wrap in let () = button "Show line number" show_line_number in let () = button "Auto indentation" auto_indent in let () = button "Auto completion" auto_complete in + let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in let () = button "Show spaces" show_spaces in let () = button "Show right margin" show_right_margin in let () = button "Show progress bar" show_progress_bar in diff --git a/ide/preferences.mli b/ide/preferences.mli index 4b04326cec..7b43079b4f 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -82,6 +82,7 @@ val show_toolbar : bool preference val window_width : int preference val window_height : int preference val auto_complete : bool preference +val auto_complete_delay : int preference val stop_before : bool preference val reset_on_tab_switch : bool preference val line_ending : line_ending preference diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index ac6712909e..396939cfcc 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -69,387 +69,101 @@ let is_substring s1 s2 = if !break then len2 - len1 else -1 -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -let complete_model_signals - (start_s : int GUtil.signal) - (update_s : (int * string * Proposals.t) GUtil.signal) - (end_s : unit GUtil.signal) : complete_model_signals = -let signals = [ - start_s#disconnect; - update_s#disconnect; - end_s#disconnect; -] in -object (self : 'a) - inherit GUtil.ml_signals signals - method start_completion = start_s#connect ~after - method update_completion = update_s#connect ~after - method end_completion = end_s#connect ~after -end - -class complete_model coqtop (buffer : GText.buffer) = - let cols = new GTree.column_list in - let column = cols#add Gobject.Data.string in - let store = GTree.list_store cols in - let filtered_store = GTree.model_filter store in - let start_completion_signal = new GUtil.signal () in - let update_completion_signal = new GUtil.signal () in - let end_completion_signal = new GUtil.signal () in -object (self) - - val signals = complete_model_signals - start_completion_signal update_completion_signal end_completion_signal - val mutable active = false - val mutable auto_complete_length = 3 - (* this variable prevents CoqIDE from autocompleting when we have deleted something *) - val mutable is_auto_completing = false - (* this mutex ensure that CoqIDE will not try to autocomplete twice *) - val mutable cache = (-1, "", Proposals.empty) - val mutable insert_offset = -1 - val mutable current_completion = ("", Proposals.empty) - val mutable lock_auto_completing = true +class completion_provider coqtop = + let self_provider = ref None in + let active = ref true in + let provider = object (self) - method connect = signals + val mutable auto_complete_length = 3 + val mutable cache = (-1, "", Proposals.empty) + val mutable insert_offset = -1 - method active = active + method name = "" - method set_active b = active <- b + method icon = None - method private handle_insert iter s = - (* we're inserting, so we may autocomplete *) - is_auto_completing <- true + method private update_proposals pref = + let (_, _, props) = cache in + let filter prop = 0 <= is_substring pref prop in + let props = Proposals.filter filter props in + props - method private handle_delete ~start ~stop = - (* disable autocomplete *) - is_auto_completing <- false - - method store = filtered_store - - method column = column - - method handle_proposal path = - let row = filtered_store#get_iter path in - let proposal = filtered_store#get ~row ~column in - let (start_offset, _, _) = cache in - (* [iter] might be invalid now, get a new one to please gtk *) - let iter = buffer#get_iter `INSERT in - (* We cancel completion when the buffer has changed recently *) - if iter#offset = insert_offset then begin - let suffix = - let len1 = String.length proposal in - let len2 = insert_offset - start_offset in - String.sub proposal len2 (len1 - len2) + method private add_proposals ctx props = + let mk text = + let item = GSourceView3.source_completion_item ~text ~label:text () in + (item :> GSourceView3.source_completion_proposal) in - buffer#begin_user_action (); - ignore (buffer#insert_interactive ~iter suffix); - buffer#end_user_action (); - end - - method private init_proposals pref props = - let () = store#clear () in - let iter prop = - let iter = store#append () in - store#set ~row:iter ~column prop - in - let () = current_completion <- (pref, props) in - Proposals.iter iter props - - method private update_proposals pref = - let (_, _, props) = cache in - let filter prop = 0 <= is_substring pref prop in - let props = Proposals.filter filter props in - let () = current_completion <- (pref, props) in - let () = filtered_store#refilter () in - props - - method private do_auto_complete k = - let iter = buffer#get_iter `INSERT in - let () = insert_offset <- iter#offset in - let log = Printf.sprintf "Completion at offset: %i" insert_offset in - let () = Minilib.log log in - let prefix = - if Gtk_parsing.ends_word iter then - let start = Gtk_parsing.find_word_start iter in - let w = buffer#get_text ~start ~stop:iter () in - if String.length w >= auto_complete_length then Some (w, start) - else None - else None - in - match prefix with - | Some (w, start) -> + let props = List.map mk (Proposals.elements props) in + ctx#add_proposals (Option.get !self_provider) props true + + method populate ctx = + let iter = ctx#iter in + let buffer = new GText.buffer iter#buffer in + let start = Gtk_parsing.find_word_start iter in + let w = start#get_text ~stop:iter in let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in let (off, prefix, props) = cache in let start_offset = start#offset in (* check whether we have the last request in cache *) if (start_offset = off) && (0 <= is_substring prefix w) then let props = self#update_proposals w in - let () = update_completion_signal#call (start_offset, w, props) in - k () + self#add_proposals ctx props else - let () = start_completion_signal#call start_offset in + let cancel = ref false in + let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in let update props = let () = cache <- (start_offset, w, props) in - let () = self#init_proposals w props in - update_completion_signal#call (start_offset, w, props) + if not !cancel then self#add_proposals ctx props in (* If not in the cache, we recompute it: first syntactic *) let synt = get_syntactic_completion buffer w Proposals.empty in (* Then semantic *) - let next prop = - let () = update prop in - Coq.lift k + let next props = + update props; + Coq.return () in let query = Coq.bind (get_semantic_completion w synt) next in (* If coqtop is computing, do the syntactic completion altogether *) - let occupied () = - let () = update synt in - k () - in + let occupied () = update synt in Coq.try_grab coqtop query occupied - | None -> end_completion_signal#call (); k () - - method private may_auto_complete () = - if active && is_auto_completing && lock_auto_completing then begin - let () = lock_auto_completing <- false in - let unlock () = lock_auto_completing <- true in - self#do_auto_complete unlock - end - - initializer - let filter_prop model row = - let (_, props) = current_completion in - let prop = store#get ~row ~column in - Proposals.mem prop props - in - let () = filtered_store#set_visible_func filter_prop in - (* Install auto-completion *) - ignore (buffer#connect#insert_text ~callback:self#handle_insert); - ignore (buffer#connect#delete_range ~callback:self#handle_delete); - ignore (buffer#connect#after#end_user_action ~callback:self#may_auto_complete); - -end - -class complete_popup (model : complete_model) (view : GText.view) = - let obj = GWindow.window ~kind:`POPUP ~show:false () in - let frame = GBin.scrolled_window - ~hpolicy:`NEVER ~vpolicy:`NEVER - ~shadow_type:`OUT ~packing:obj#add () - in -(* let frame = GBin.frame ~shadow_type:`OUT ~packing:obj#add () in *) - let data = GTree.view - ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment - ~rules_hint:true ~headers_visible:false - ~model:model#store ~packing:frame#add () - in - let renderer = GTree.cell_renderer_text [], ["text", model#column] in - let col = GTree.view_column ~renderer () in - let _ = data#append_column col in - let () = col#set_sizing `AUTOSIZE in - let page_size = 16 in - -object (self) - - method coerce = view#coerce - - method private refresh_style () = - let (renderer, _) = renderer in - let font = Pango.Font.from_string Preferences.text_font#get in - renderer#set_properties [`FONT_DESC font; `XPAD 10] - - method private coordinates pos = - (* Toplevel position w.r.t. screen *) - let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in - (* Position of view w.r.t. window *) - let (ux, uy) = Gdk.Window.get_position view#misc#window in - (* Relative buffer position to view *) - let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in - (* Iter position *) - let iter = view#buffer#get_iter pos in - let coords = view#get_iter_location iter in - let lx = Gdk.Rectangle.x coords in - let ly = Gdk.Rectangle.y coords in - let w = Gdk.Rectangle.width coords in - let h = Gdk.Rectangle.height coords in - (* Absolute position *) - (x + lx + ux - dx, y + ly + uy - dy, w, h) - - method private select_any f = - let sel = data#selection#get_selected_rows in - let path = match sel with - | [] -> - begin match model#store#get_iter_first with - | None -> None - | Some iter -> Some (model#store#get_path iter) - end - | path :: _ -> Some path - in - match path with - | None -> () - | Some path -> - let path = f path in - let _ = data#selection#select_path path in - data#scroll_to_cell ~align:(0.,0.) path col - - method private select_previous () = - let prev path = - let copy = GTree.Path.copy path in - if GTree.Path.prev path then path - else copy - in - self#select_any prev - - method private select_next () = - let next path = - let () = GTree.Path.next path in - path - in - self#select_any next - method private select_previous_page () = - let rec up i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up (pred i) path - else copy - in - self#select_any (up page_size) + method matched ctx = + if !active then + let iter = ctx#iter in + let () = insert_offset <- iter#offset in + let log = Printf.sprintf "Completion at offset: %i" insert_offset in + let () = Minilib.log log in + if Gtk_parsing.ends_word iter#backward_char then + let start = Gtk_parsing.find_word_start iter in + iter#offset - start#offset >= auto_complete_length + else false + else false - method private select_next_page () = - let rec down i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (pred i) (model#store#get_path iter) - else copy - in - self#select_any (down page_size) + method activation = [`INTERACTIVE; `USER_REQUESTED] - method private select_first () = - let rec up path = - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up path - else copy - in - self#select_any up + method info_widget proposal = None - method private select_last () = - let rec down path = - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (model#store#get_path iter) - else copy - in - self#select_any down + method update_info proposal info = () - method private select_enter () = - let sel = data#selection#get_selected_rows in - match sel with - | [] -> () - | path :: _ -> - let () = model#handle_proposal path in - self#hide () + method start_iter ctx proposal iter = false - method proposal = - let sel = data#selection#get_selected_rows in - if obj#misc#visible then match sel with - | [] -> None - | path :: _ -> - let row = model#store#get_iter path in - let column = model#column in - let proposal = model#store#get ~row ~column in - Some proposal - else None + method activate_proposal proposal iter = false - method private manage_scrollbar () = - (* HACK: we don't have access to the treeview size because of the lack of - LablGTK binding for certain functions, so we bypass it by approximating - it through the size of the proposals *) - let height = match model#store#get_iter_first with - | None -> -1 - | Some iter -> - let path = model#store#get_path iter in - let area = data#get_cell_area ~path ~col () in - let height = Gdk.Rectangle.height area in - let height = page_size * height in - height - in - let len = ref 0 in - let () = model#store#foreach (fun _ _ -> incr len; false) in - if !len > page_size then - let () = frame#set_vpolicy `ALWAYS in - data#misc#set_size_request ~height () - else - data#misc#set_size_request ~height:(-1) () + method interactive_delay = (-1) - method private refresh () = - let () = frame#set_vpolicy `NEVER in - let () = self#select_first () in - let () = obj#misc#show () in - let () = self#manage_scrollbar () in - obj#resize ~width:1 ~height:1 + method priority = 0 - method private start_callback off = - let (x, y, w, h) = self#coordinates (`OFFSET off) in - let () = obj#move ~x ~y:(y + 3 * h / 2) in - () + end in + let provider = GSourceView3.source_completion_provider provider in + object (self) - method private update_callback (off, word, props) = - if Proposals.is_empty props then self#hide () - else if Proposals.mem word props then self#hide () - else self#refresh () + inherit GSourceView3.source_completion_provider provider#as_source_completion_provider - method private end_callback () = - obj#misc#hide () + method active = !active - method private hide () = self#end_callback () + method set_active b = active := b - initializer - let move_cb _ _ ~extend = self#hide () in - let key_cb ev = - let eval cb = cb (); true in - let ev_key = GdkEvent.Key.keyval ev in - if obj#misc#visible then - if ev_key = GdkKeysyms._Up then eval self#select_previous - else if ev_key = GdkKeysyms._Down then eval self#select_next - else if ev_key = GdkKeysyms._Tab then eval self#select_enter - else if ev_key = GdkKeysyms._Return then eval self#select_enter - else if ev_key = GdkKeysyms._Escape then eval self#hide - else if ev_key = GdkKeysyms._Page_Down then eval self#select_next_page - else if ev_key = GdkKeysyms._Page_Up then eval self#select_previous_page - else if ev_key = GdkKeysyms._Home then eval self#select_first - else if ev_key = GdkKeysyms._End then eval self#select_last - else false - else false - in - (* Style handling *) - let _ = view#misc#connect#style_set ~callback:self#refresh_style in - let _ = self#refresh_style () in - let _ = data#set_resize_mode `PARENT in - let _ = frame#set_resize_mode `PARENT in - (* Callback to model *) - let _ = model#connect#start_completion ~callback:self#start_callback in - let _ = model#connect#update_completion ~callback:self#update_callback in - let _ = model#connect#end_completion ~callback:self#end_callback in - (* Popup interaction *) - let _ = view#event#connect#key_press ~callback:key_cb in - (* Hiding the popup when necessary*) - let _ = view#misc#connect#hide ~callback:obj#misc#hide in - let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in - let _ = view#connect#move_cursor ~callback:move_cb in - let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in - () + initializer + self_provider := Some (self :> GSourceView3.source_completion_provider) -end + end diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index ac9e6cd94f..020fe26cfb 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -10,27 +10,9 @@ module Proposals : sig type t end -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -class complete_model : Coq.coqtop -> GText.buffer -> +class completion_provider : Coq.coqtop -> object + inherit GSourceView3.source_completion_provider method active : bool - method connect : complete_model_signals method set_active : bool -> unit - method store : GTree.model_filter - method column : string GTree.column - method handle_proposal : Gtk.tree_path -> unit -end - -class complete_popup : complete_model -> GText.view -> -object - method coerce : GObj.widget - method proposal : string option end diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 769ce61ee1..b7a35d7e94 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -287,18 +287,17 @@ end class script_view (tv : source_view) (ct : Coq.coqtop) = let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in -let completion = new Wg_Completion.complete_model ct view#buffer in -let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in +let provider = new Wg_Completion.completion_provider ct in object (self) inherit GSourceView3.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer - method auto_complete = completion#active + method auto_complete = provider#active method set_auto_complete flag = - completion#set_active flag + provider#set_active flag method recenter_insert = self#scroll_to_mark @@ -448,7 +447,7 @@ object (self) self#buffer#delete_mark (`MARK insert_mark) - method complete_popup = popup + method proposal : string option = None (* FIXME *) method undo = undo_manager#undo method redo = undo_manager#redo @@ -527,10 +526,15 @@ object (self) stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs; stick tab_length self self#set_tab_width; stick auto_complete self self#set_auto_complete; + stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d); let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in stick text_font self cb; + let () = self#completion#set_accelerators 0 in + let () = self#completion#set_show_headers false in + let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in + () end diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 91c8e758a5..4b6591e063 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -28,7 +28,7 @@ object method uncomment : unit -> unit method apply_unicode_binding : unit -> unit method recenter_insert : unit - method complete_popup : Wg_Completion.complete_popup + method proposal : string option end val script_view : Coq.coqtop -> diff --git a/interp/impargs.ml b/interp/impargs.ml index df28b32f81..e2c732809a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -646,11 +646,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l -(* TODO: either turn these warnings on and document them, or handle these cases sensibly *) -let warn_set_maximal_deprecated = - CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated" - (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal")) +let msg_trailing_implicit id = + user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].")) type implicit_kind = Implicit | MaximallyImplicit | NotImplicit @@ -662,7 +660,7 @@ let compute_implicit_statuses autoimps l = | Name id :: autoimps, Implicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality imps' false in - if max then warn_set_maximal_deprecated i; + if max then msg_trailing_implicit id; Some (ExplByName id, Manual, (max, true)) :: imps' | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> user_err ~hdr:"set_implicits" diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 261a3510d6..cebbfe4986 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -144,11 +144,11 @@ let abstract_context hyps = in Context.Named.fold_outside fold hyps ~init:([], []) -let abstract_constant_type t (hyps, subst) = +let abstract_as_type t (hyps, subst) = let t = Vars.subst_vars subst t in List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps -let abstract_constant_body c (hyps, subst) = +let abstract_as_body c (hyps, subst) = let c = Vars.subst_vars subst c in it_mkLambda_or_LetIn c hyps @@ -192,8 +192,7 @@ let discharge_abstract_universe_context subst abs_ctx auctx = let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in subst, (AUContext.union abs_ctx auctx) -let lift_univs cb subst auctx0 = - match cb.const_universes with +let lift_univs subst auctx0 = function | Monomorphic ctx -> assert (AUContext.is_empty auctx0); subst, (Monomorphic ctx) @@ -219,7 +218,7 @@ let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) = let expmod = expmod_constr_subst cache modlist usubst in let hyps = Context.Named.map expmod abstract in let hyps = abstract_context hyps in - let c = abstract_constant_body (expmod c) hyps in + let c = abstract_as_body (expmod c) hyps in (c, priv) let cook_constr infos c = @@ -230,11 +229,11 @@ let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in - let usubst, univs = lift_univs cb usubst abs_ctx in + let usubst, univs = lift_univs usubst abs_ctx cb.const_universes in let expmod = expmod_constr_subst cache modlist usubst in let hyps0 = Context.Named.map expmod abstract in let hyps = abstract_context hyps0 in - let map c = abstract_constant_body (expmod c) hyps in + let map c = abstract_as_body (expmod c) hyps in let body = match cb.const_body with | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) @@ -243,7 +242,7 @@ let cook_constant { from = cb; info } = | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in - let typ = abstract_constant_type (expmod cb.const_type) hyps in + let typ = abstract_as_type (expmod cb.const_type) hyps in { cook_body = body; cook_type = typ; @@ -259,104 +258,160 @@ let cook_constant { from = cb; info } = (********************************) (* Discharging mutual inductive *) -(* Replace - - Var(y1)..Var(yq):C1..Cq |- Ij:Bj - Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti - - by - - |- Ij: (y1..yq:C1..Cq)Bj - I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] -*) - -let it_mkNamedProd_wo_LetIn b d = - List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d - -let abstract_inductive decls nparamdecls inds = - let open Entries in - let ntyp = List.length inds in - let ndecls = Context.Named.length decls in - let args = Context.Named.to_instance mkVar (List.rev decls) in - let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (Vars.substl subs) lc in - let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to cook_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - params +let template_level_of_var ~template_check d = + (* When [template_check], a universe from a section variable may not + be in the universes from the inductive (it must be pre-declared) + so always [None]. *) + if template_check then None + else + let c = Term.strip_prod_assum (RelDecl.get_type d) in + match kind c with + | Sort (Type u) -> Univ.Universe.level u + | _ -> None + +let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c) + +let abstract_rel_ctx (section_decls,subst) ctx = + (* Dealing with substitutions between contexts is too annoying, so + we reify [ctx] into a big [forall] term and work on that. *) + let t = it_mkProd_or_LetIn mkProp ctx in + let t = Vars.subst_vars subst t in + let t = it_mkProd_wo_LetIn t section_decls in + let ctx, t = decompose_prod_assum t in + assert (Constr.equal t mkProp); + ctx + +let abstract_lc ~ntypes expmod (newparams,subst) c = + let args = Array.rev_of_list (CList.map_filter (fun d -> + if RelDecl.is_local_def d then None + else match RelDecl.get_name d with + | Anonymous -> assert false + | Name id -> Some (mkVar id)) + newparams) in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true + let diff = List.length newparams in + let subs = List.init ntypes (fun k -> + lift diff (mkApp (mkRel (k+1), args))) + in + let c = Vars.substl subs c in + let c = Vars.subst_vars subst (expmod c) in + let c = it_mkProd_wo_LetIn c newparams in + c + +let abstract_projection ~params expmod hyps t = + let t = it_mkProd_or_LetIn t params in + let t = mkArrowR mkProp t in (* dummy type standing in for the inductive *) + let t = abstract_as_type (expmod t) hyps in + let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in + t + +let cook_one_ind ~template_check ~ntypes + (section_decls,_ as hyps) expmod mip = + let mind_arity = match mip.mind_arity with + | RegularArity {mind_user_arity=arity;mind_sort=sort} -> + let arity = abstract_as_type (expmod arity) hyps in + let sort = destSort (expmod (mkSort sort)) in + RegularArity {mind_user_arity=arity; mind_sort=sort} + | TemplateArity {template_param_levels=levels;template_level} -> + let sec_levels = CList.map_filter (fun d -> + if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d) + else None) + section_decls + in + let levels = List.rev_append sec_levels levels in + TemplateArity {template_param_levels=levels;template_level} + in + let mind_arity_ctxt = + let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in + abstract_rel_ctx hyps ctx + in + let mind_user_lc = + Array.map (abstract_lc ~ntypes expmod hyps) + mip.mind_user_lc + in + let mind_nf_lc = Array.map (fun (ctx,t) -> + let lc = it_mkProd_or_LetIn t ctx in + let lc = abstract_lc ~ntypes expmod hyps lc in + decompose_prod_assum lc) + mip.mind_nf_lc + in + { mind_typename = mip.mind_typename; + mind_arity_ctxt; + mind_arity; + mind_consnames = mip.mind_consnames; + mind_user_lc; + mind_nrealargs = mip.mind_nrealargs; + mind_nrealdecls = mip.mind_nrealdecls; + mind_kelim = mip.mind_kelim; + mind_nf_lc; + mind_consnrealargs = mip.mind_consnrealargs; + mind_consnrealdecls = mip.mind_consnrealdecls; + mind_recargs = mip.mind_recargs; (* TODO is this correct? checker should tell us. *) + mind_relevance = mip.mind_relevance; + mind_nb_constant = mip.mind_nb_constant; + mind_nb_args = mip.mind_nb_args; + mind_reloc_tbl = mip.mind_reloc_tbl; + } let cook_inductive { Opaqueproof.modlist; abstract } mib = - let open Entries in let (section_decls, subst, abs_uctx) = abstract in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx - | Polymorphic auctx -> - let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in - let subst = Univ.make_instance_subst subst in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_entry (nas, auctx) - in + let subst, mind_universes = lift_univs subst abs_uctx mib.mind_universes in let cache = RefTable.create 13 in - let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in - let inds = - Array.map_to_list - (fun mip -> - let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = discharge ty in - let lc = Array.map discharge mip.mind_user_lc in - (mip.mind_typename, - arity, template, - Array.to_list mip.mind_consnames, - Array.to_list lc)) - mib.mind_packets in - let section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | PrimRecord info -> - Some (Some (Array.map (fun (x,_,_,_) -> x) info)) - | FakeRecord -> Some None - | NotRecord -> None + let expmod = expmod_constr_subst cache modlist subst in + let section_decls = Context.Named.map expmod section_decls in + let removed_vars = Context.Named.to_vars section_decls in + let section_decls, _ as hyps = abstract_context section_decls in + let nnewparams = Context.Rel.nhyps section_decls in + let template_check = mib.mind_typing_flags.check_template in + let mind_params_ctxt = + let ctx = Context.Rel.map expmod mib.mind_params_ctxt in + abstract_rel_ctx hyps ctx + in + let ntypes = mib.mind_ntypes in + let mind_packets = + Array.map (cook_one_ind ~template_check ~ntypes hyps expmod) + mib.mind_packets in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_cumulative = Option.has_some mib.mind_variance; - mind_entry_universes = ind_univs + let mind_record = match mib.mind_record with + | NotRecord -> NotRecord + | FakeRecord -> FakeRecord + | PrimRecord data -> + let data = Array.map (fun (id,projs,relevances,tys) -> + let tys = Array.map (abstract_projection ~params:mib.mind_params_ctxt expmod hyps) tys in + (id,projs,relevances,tys)) + data + in + PrimRecord data + in + let mind_hyps = + List.filter (fun d -> not (Id.Set.mem (NamedDecl.get_id d) removed_vars)) + mib.mind_hyps + in + let mind_variance, mind_sec_variance = + match mib.mind_variance, mib.mind_sec_variance with + | None, None -> None, None + | None, Some _ | Some _, None -> assert false + | Some variance, Some sec_variance -> + let sec_variance, newvariance = + Array.chop (Array.length sec_variance - AUContext.size abs_uctx) + sec_variance + in + Some (Array.append newvariance variance), Some sec_variance + in + { + mind_packets; + mind_record; + mind_finite = mib.mind_finite; + mind_ntypes = mib.mind_ntypes; + mind_hyps; + mind_nparams = mib.mind_nparams + nnewparams; + mind_nparams_rec = mib.mind_nparams_rec + nnewparams; + mind_params_ctxt; + mind_universes; + mind_variance; + mind_sec_variance; + mind_private = mib.mind_private; + mind_typing_flags = mib.mind_typing_flags; } let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 83a8b9edfc..c2d47735ec 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -31,7 +31,7 @@ val cook_constr : Opaqueproof.cooking_info list -> (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) val cook_inductive : - Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry + Opaqueproof.cooking_info -> mutual_inductive_body -> mutual_inductive_body (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9fd10b32e6..0b6e59bd5e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -223,6 +223,11 @@ type mutual_inductive_body = { mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) + mind_sec_variance : Univ.Variance.t array option; + (** Variance info for section polymorphic universes. [None] + outside sections. The final variance once all sections are + discharged is [mind_sec_variance ++ mind_variance]. *) + mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 35185b6a5e..27e3f84464 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -248,6 +248,7 @@ let subst_mind_body sub mib = mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; mind_variance = mib.mind_variance; + mind_sec_variance = mib.mind_sec_variance; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index b19472dc99..591cd050a5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -276,7 +276,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let typecheck_inductive env (mie:mutual_inductive_entry) = +let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") | _ -> () @@ -335,8 +335,19 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = data, Some None in - (* TODO pass only the needed bits *) - let variance = InferCumulativity.infer_inductive env mie in + let variance = if not mie.mind_entry_cumulative then None + else match mie.mind_entry_universes with + | Monomorphic_entry _ -> + CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.") + | Polymorphic_entry (_,uctx) -> + let univs = Instance.to_array @@ UContext.instance uctx in + let univs = match sec_univs with + | None -> univs + | Some sec_univs -> Array.append sec_univs univs + in + let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in + Some variances + in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 5c04e860a2..8dea8f046d 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -17,6 +17,7 @@ open Declarations - environment with inductives + parameters in rel context - abstracted universes - checked variance info + (variance for section universes is at the beginning of the array) - record entry (checked to be OK) - parameters - for each inductive, @@ -24,9 +25,11 @@ open Declarations * (indices * splayed constructor types) (both without params) * top allowed elimination *) -val typecheck_inductive : env -> mutual_inductive_entry -> - env - * universes * Univ.Variance.t array option +val typecheck_inductive : env -> sec_univs:Univ.Level.t array option + -> mutual_inductive_entry + -> env + * universes + * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context * ((inductive_arity * Constr.types array) * diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0d900c2ec9..3771454db5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -466,7 +466,8 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env ~sec_univs names prv univs variance + paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env paramsctxt inds in @@ -517,6 +518,15 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_reloc_tbl = rtbl; } in let packets = Array.map3 build_one_packet names inds recargs in + let variance, sec_variance = match variance with + | None -> None, None + | Some variance -> match sec_univs with + | None -> Some variance, None + | Some sec_univs -> + let nsec = Array.length sec_univs in + Some (Array.sub variance nsec (Array.length variance - nsec)), + Some (Array.sub variance 0 nsec) + in let mib = (* Build the mutual inductive *) { mind_record = NotRecord; @@ -529,6 +539,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite mind_packets = packets; mind_universes = univs; mind_variance = variance; + mind_sec_variance = sec_variance; mind_private = prv; mind_typing_flags = Environ.typing_flags env; } @@ -549,9 +560,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (************************************************************************) (************************************************************************) -let check_inductive env kn mie = +let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in + let (env_ar_par, univs, variance, record, paramsctxt, inds) = + IndTyping.typecheck_inductive env ~sec_univs mie + in (* Then check positivity conditions *) let chkpos = (Environ.typing_flags env).check_positive in let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames) @@ -562,6 +575,6 @@ let check_inductive env kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 240ba4e2bb..9b54e8b878 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,4 +14,5 @@ open Environ open Entries (** Check an inductive. *) -val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body +val check_inductive : env -> sec_univs:Univ.Level.t array option + -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 77abe6b410..211c909241 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -188,15 +188,12 @@ let infer_arity_constructor is_arity env variances arcn = open Entries -let infer_inductive_core env params entries uctx = - let uarray = Instance.to_array @@ UContext.instance uctx in - if Array.is_empty uarray then raise TrivialVariance; - let env = Environ.push_context uctx env in +let infer_inductive_core env univs entries = + if Array.is_empty univs then raise TrivialVariance; let variances = Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) - LMap.empty uarray + LMap.empty univs in - let env, _ = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity @@ -210,17 +207,8 @@ let infer_inductive_core env params entries uctx = | exception Not_found -> Invariant | IrrelevantI -> Irrelevant | CovariantI -> Covariant) - uarray - -let infer_inductive env mie = - let open Entries in - let params = mie.mind_entry_params in - let entries = mie.mind_entry_inds in - if not mie.mind_entry_cumulative then None - else - let uctx = match mie.mind_entry_universes with - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> uctx - in - try Some (infer_inductive_core env params entries uctx) - with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) + univs + +let infer_inductive ~env_params univs entries = + try infer_inductive_core env_params univs entries + with TrivialVariance -> Array.make (Array.length univs) Invariant diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index 2bddfe21e2..a8f593c7f9 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -8,5 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> - Univ.Variance.t array option +val infer_inductive + : env_params:Environ.env + (** Environment containing the polymorphic universes and the + parameters. *) + -> Univ.Level.t array + (** Universes whose cumulativity we want to infer. *) + -> Entries.one_inductive_entry list + (** The inductive block data we want to infer cumulativity for. + NB: we ignore the template bool and the names, only the terms + are used. *) + -> Univ.Variance.t array diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ee101400d6..f6f2058c13 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -908,14 +908,19 @@ let check_mind mie lab = (* The label and the first inductive type name should match *) assert (Id.equal (Label.to_id lab) oie.mind_entry_typename) +let add_checked_mind kn mib senv = + let mib = + match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + in + add_field (MutInd.label kn,SFBmind mib) (I kn) senv + let add_mind l mie senv = let () = check_mind mie l in let kn = MutInd.make2 senv.modpath l in - let mib = Indtypes.check_inductive senv.env kn mie in - let mib = - match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + let sec_univs = Option.map Section.all_poly_univs senv.sections in - kn, add_field (l,SFBmind mib) (I kn) senv + let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in + kn, add_checked_mind kn mib senv (** Insertion of module types *) @@ -1014,9 +1019,8 @@ let close_section senv = add_constant_aux senv (kn, cb) | `Inductive (ind, mib) -> let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in - let mie = Cooking.cook_inductive info mib in - let _, senv = add_mind (MutInd.label ind) mie senv in - senv + let mib = Cooking.cook_inductive info mib in + add_checked_mind ind mib senv in List.fold_left fold senv redo diff --git a/kernel/section.ml b/kernel/section.ml index 603ef5d006..6fa0543b23 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -28,6 +28,8 @@ type 'a t = { sec_mono_universes : ContextSet.t; sec_poly_universes : Name.t array * UContext.t; (** Universes local to the section *) + all_poly_univs : Univ.Level.t array; + (** All polymorphic universes, including from previous sections. *) has_poly_univs : bool; (** Are there polymorphic universes or constraints, including in previous sections. *) sec_entries : section_entry list; @@ -41,6 +43,8 @@ let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth p let has_poly_univs sec = sec.has_poly_univs +let all_poly_univs sec = sec.all_poly_univs + let find_emap e (cmap, imap) = match e with | SecDefinition con -> Cmap.find con cmap | SecInductive ind -> Mindmap.find ind imap @@ -57,7 +61,10 @@ let push_context (nas, ctx) sec = else let (snas, sctx) = sec.sec_poly_universes in let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in - { sec with sec_poly_universes; has_poly_univs = true } + let all_poly_univs = + Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx) + in + { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true } let rec is_polymorphic_univ u sec = let (_, uctx) = sec.sec_poly_universes in @@ -81,6 +88,7 @@ let open_section ~custom sec_prev = sec_context = 0; sec_mono_universes = ContextSet.empty; sec_poly_universes = ([||], UContext.empty); + all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev; has_poly_univs = Option.cata has_poly_univs false sec_prev; sec_entries = []; sec_data = (Cmap.empty, Mindmap.empty); diff --git a/kernel/section.mli b/kernel/section.mli index fbd3d8254e..37d0dab317 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -57,6 +57,14 @@ val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t (** {6 Retrieving section data} *) +val all_poly_univs : 'a t -> Univ.Level.t array +(** Returns all polymorphic universes, including those from previous + sections. Earlier sections are earlier in the array. + + NB: even if the array is empty there may be polymorphic + constraints about monomorphic universes, which prevent declaring + monomorphic globals. *) + type abstr_info = private { abstr_ctx : Constr.named_context; (** Section variables of this prefix *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 0029ff96d5..0712774576 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -345,8 +345,8 @@ struct (Level.is_prop u && not (Level.is_sprop v)) else false - let successor (u,n) = - if Level.is_small u then type1 + let successor (u,n as e) = + if is_small e then type1 else (u, n + 1) let addn k (u,n as x) = @@ -755,6 +755,10 @@ struct | Invariant, _ | _, Invariant -> Invariant | Covariant, Covariant -> Covariant + let equal a b = match a,b with + | Irrelevant, Irrelevant | Covariant, Covariant | Invariant, Invariant -> true + | (Irrelevant | Covariant | Invariant), _ -> false + let check_subtype x y = match x, y with | (Irrelevant | Covariant | Invariant), Irrelevant -> true | Irrelevant, Covariant -> false diff --git a/kernel/univ.mli b/kernel/univ.mli index ccb5c80cbf..f7c984870f 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -263,6 +263,8 @@ sig val pr : t -> Pp.t + val equal : t -> t -> bool + end (** {6 Universe instances} *) @@ -320,7 +322,7 @@ val in_punivs : 'a -> 'a puniverses val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool (** A vector of universe levels with universe Constraint.t, - representiong local universe variables and associated Constraint.t *) + representing local universe variables and associated Constraint.t *) module UContext : sig diff --git a/library/lib.ml b/library/lib.ml index 9cce9b92ad..7f96adeecf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -500,7 +500,7 @@ let close_section () = type frozen = lib_state -let freeze ~marshallable = !lib_state +let freeze () = !lib_state let unfreeze st = lib_state := st diff --git a/library/lib.mli b/library/lib.mli index 0d03046dc2..1fe72389f6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -151,7 +151,7 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:bool -> frozen +val freeze : unit -> frozen val unfreeze : frozen -> unit (** Keep only the libobject structure, not the objects themselves *) diff --git a/library/states.ml b/library/states.ml index 0be153d96a..90303a2a5c 100644 --- a/library/states.ml +++ b/library/states.ml @@ -18,7 +18,7 @@ let replace_summary (lib,_) st = lib, st let replace_lib (_,st) lib = lib, st let freeze ~marshallable = - (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) + (Lib.freeze (), Summary.freeze_summaries ~marshallable) let unfreeze (fl,fs) = Lib.unfreeze fl; diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index 97f6fe0613..edfb5a2a94 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -523,3 +523,22 @@ Instance SatProdPos : Saturate Z.mul := SatOk := Z.mul_pos_pos |}. Add Saturate SatProdPos. + +Lemma pow_pos_strict : + forall a b, + 0 < a -> 0 < b -> 0 < a ^ b. +Proof. + intros. + apply Z.pow_pos_nonneg; auto. + apply Z.lt_le_incl;auto. +Qed. + + +Instance SatPowPos : Saturate Z.pow := + {| + PArg1 := fun x => 0 < x; + PArg2 := fun y => 0 < y; + PRes := fun r => 0 < r; + SatOk := pow_pos_strict + |}. +Add Saturate SatPowPos. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index cb15274736..61234145e1 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -395,50 +395,40 @@ let saturate_by_linear_equalities sys = output_sys sys output_sys sys'; sys' -(* let saturate_linear_equality_non_linear sys0 = - let (l,_) = extract_all (is_substitution false) sys0 in - let rec elim l acc = - match l with - | [] -> acc - | (v,pc)::l' -> - let nc = saturate (non_linear_pivot sys0 pc v) (sys0@acc) in - elim l' (nc@acc) in - elim l [] - *) - -let bounded_vars (sys : WithProof.t list) = - let l = fst (extract_all (fun ((p, o), prf) -> LinPoly.is_variable p) sys) in - List.fold_left (fun acc (i, wp) -> IMap.add i wp acc) IMap.empty l - -let rec power n p = if n = 1 then p else WithProof.product p (power (n - 1) p) - -let bound_monomial mp m = - if Monomial.is_var m || Monomial.is_const m then None - else - try - Some - (Monomial.fold - (fun v i acc -> - let wp = IMap.find v mp in - WithProof.product (power i wp) acc) - m (WithProof.const (Int 1))) - with Not_found -> None - let bound_monomials (sys : WithProof.t list) = - let mp = bounded_vars sys in - let m = + let l = + extract_all + (fun ((p, o), _) -> + match LinPoly.get_bound p with + | None -> None + | Some Vect.Bound.{cst; var; coeff} -> + Some (Monomial.degree (LinPoly.MonT.retrieve var))) + sys + in + let deg = + List.fold_left (fun acc ((p, o), _) -> max acc (LinPoly.degree p)) 0 sys + in + let vars = List.fold_left - (fun acc ((p, _), _) -> - Vect.fold - (fun acc v _ -> - let m = LinPoly.MonT.retrieve v in - match bound_monomial mp m with - | None -> acc - | Some r -> IMap.add v r acc) - acc p) - IMap.empty sys + (fun acc ((p, o), _) -> ISet.union (LinPoly.monomials p) acc) + ISet.empty sys + in + let bounds = + saturate_bin + (fun (i1, w1) (i2, w2) -> + if i1 + i2 > deg then None + else + match WithProof.mul_bound w1 w2 with + | None -> None + | Some b -> Some (i1 + i2, b)) + (fst l) + in + let has_mon (_, ((p, o), _)) = + match LinPoly.get_bound p with + | None -> false + | Some Vect.Bound.{cst; var; coeff} -> ISet.mem var vars in - IMap.fold (fun _ e acc -> e :: acc) m [] + List.map snd (List.filter has_mon bounds) @ snd l let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 03f042647c..160b492d3d 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -140,6 +140,25 @@ let saturate p f sys = Printexc.print_backtrace stdout; raise x +let saturate_bin (f : 'a -> 'a -> 'a option) (l : 'a list) = + let rec map_with acc e l = + match l with + | [] -> acc + | e' :: l' -> ( + match f e e' with + | None -> map_with acc e l' + | Some r -> map_with (r :: acc) e l' ) + in + let rec map2_with acc l' = + match l' with [] -> acc | e' :: l' -> map2_with (map_with acc e' l) l' + in + let rec iterate acc l' = + match map2_with [] l' with + | [] -> List.rev_append l' acc + | res -> iterate (List.rev_append l' acc) res + in + iterate [] l + open Num open Big_int diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index ef8d154b13..5dcaf3be44 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -116,6 +116,7 @@ val simplify : ('a -> 'a option) -> 'a list -> 'a list option val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list +val saturate_bin : ('a -> 'a -> 'a option) -> 'a list -> 'a list val generate : ('a -> 'b option) -> 'a list -> 'b list val app_funs : ('a -> 'b option) list -> 'a -> 'b option val command : string -> string array -> 'a -> 'b diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index a4f9b60b14..b20213979b 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -379,6 +379,8 @@ module LinPoly = struct else acc) [] l + let get_bound p = Vect.Bound.of_vect p + let min_list (l : int list) = match l with [] -> None | e :: l -> Some (List.fold_left min e l) @@ -892,8 +894,9 @@ module WithProof = struct if Vect.is_null r && n >/ Int 0 then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) else ( - Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output - ((p1, o1), prf1); + if debug then + Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output + ((p1, o1), prf1); raise InvalidProof ) let cutting_plane ((p, o), prf) = @@ -1027,6 +1030,31 @@ module WithProof = struct else None in saturate select gen sys0 + + open Vect.Bound + + let mul_bound w1 w2 = + let (p1, o1), prf1 = w1 in + let (p2, o2), prf2 = w2 in + match (LinPoly.get_bound p1, LinPoly.get_bound p2) with + | None, _ | _, None -> None + | ( Some {cst = c1; var = v1; coeff = c1'} + , Some {cst = c2; var = v2; coeff = c2'} ) -> ( + let good_coeff b o = + match o with + | Eq -> Some (minus_num b) + | _ -> if b <=/ Int 0 then Some (minus_num b) else None + in + match (good_coeff c1 o2, good_coeff c2 o1) with + | None, _ | _, None -> None + | Some c1, Some c2 -> + let ext_mult c w = + if c =/ Int 0 then zero else mult (LinPoly.constant c) w + in + Some + (addition + (addition (product w1 w2) (ext_mult c1 w2)) + (ext_mult c2 w1)) ) end (* Local Variables: *) diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 7e905ac69b..4b56b037e0 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -224,6 +224,8 @@ module LinPoly : sig p is linear in x i.e x does not occur in b and a is a constant such that [pred a] *) + val get_bound : t -> Vect.Bound.t option + val product : t -> t -> t (** [product p q] @return the product of the polynomial [p*q] *) @@ -372,4 +374,5 @@ module WithProof : sig val saturate_subst : bool -> t list -> t list val is_substitution : bool -> t -> var option + val mul_bound : t -> t -> t option end diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 2db674d397..97fffbd7c8 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -26,6 +26,10 @@ open Context.Rel.Declaration exception Find_at of int +(* timing *) + +let timing_enabled = ref false + (* profiling *) let profiling_enabled = ref false @@ -79,6 +83,12 @@ let get_profiling_enabled () = let set_profiling_enabled b = profiling_enabled := b +let get_timing_enabled () = + !timing_enabled + +let set_timing_enabled b = + timing_enabled := b + let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do @@ -496,19 +506,23 @@ let native_norm env sigma c ty = let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in let profile = get_profiling_enabled () in + let print_timing = get_timing_enabled () in + let tc0 = Sys.time () in let fn = Nativelib.compile ml_filename code ~profile:profile in - if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); + let tc1 = Sys.time () in + let time_info = Format.sprintf "native_compute: Compilation done in %.5f@." (tc1 -. tc0) in + if print_timing then Feedback.msg_info (Pp.str time_info); let profiler_pid = if profile then start_profiler () else None in let t0 = Sys.time () in Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd); let t1 = Sys.time () in if profile then stop_profiler profiler_pid; - let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + let time_info = Format.sprintf "native_compute: Evaluation done in %.5f@." (t1 -. t0) in + if print_timing then Feedback.msg_info (Pp.str time_info); let res = nf_val env sigma !Nativelib.rt1 ty in let t2 = Sys.time () in - let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + let time_info = Format.sprintf "native_compute: Reification done in %.5f@." (t2 -. t1) in + if print_timing then Feedback.msg_info (Pp.str time_info); EConstr.of_constr res let native_conv_generic pb sigma t = diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index 02de034fcb..458fe70e2c 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -20,6 +20,9 @@ val set_profile_filename : string -> unit val get_profiling_enabled : unit -> bool val set_profiling_enabled : bool -> unit +val get_timing_enabled : unit -> bool +val set_timing_enabled : bool -> unit + val native_norm : env -> evar_map -> constr -> types -> constr diff --git a/stm/stm.ml b/stm/stm.ml index eff2403eca..4c539684e3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2362,7 +2362,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze ~marshallable:false in + st, Lib.freeze () in let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () diff --git a/tactics/declare.ml b/tactics/declare.ml index da4de3df77..9a14f4d40f 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -362,7 +362,7 @@ let inVariable : unit -> obj = classify_function = (fun () -> Dispose)} let declare_variable ~name ~kind d = - (* Constr raisonne sur les noms courts *) + (* Variables are distinguished by only short names *) if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index d6fda00ad8..6cdb24965d 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind = let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) else - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma) let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v new file mode 100644 index 0000000000..87f15a4a19 --- /dev/null +++ b/test-suite/bugs/closed/bug_11133.v @@ -0,0 +1,18 @@ +Module Type Universe. +Parameter U : nat. +End Universe. + +Module Univ_prop (Univ : Universe). +Include Univ. +End Univ_prop. + +Module Monad (Univ : Universe). +Module UP := (Univ_prop Univ). +End Monad. + +Module Rules (Univ:Universe). +Module MP := Monad Univ. +Include MP. +Import UP. +Definition M := UP.U. (* anomaly here *) +End Rules. diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v new file mode 100644 index 0000000000..6e109e33e6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11168.v @@ -0,0 +1,5 @@ +Axiom f : forall T, T. +Arguments f &. +Check f _ _. +Check f (_ -> _) _. +Check f (forall x, _) _. diff --git a/test-suite/bugs/closed/bug_11421.v b/test-suite/bugs/closed/bug_11421.v new file mode 100644 index 0000000000..8ddf05c888 --- /dev/null +++ b/test-suite/bugs/closed/bug_11421.v @@ -0,0 +1 @@ +Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}. diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v index ff08bdc6bb..52cc34beb3 100644 --- a/test-suite/bugs/closed/bug_2729.v +++ b/test-suite/bugs/closed/bug_2729.v @@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse) (p : pu_type from mid) (qs : SequenceBase pu mid to), SequenceBase pu from to. -Arguments Nil [pu cxt]. +Arguments Nil {pu cxt}. Arguments Cons [pu from mid to]. Program Fixpoint insertBase {pu : PatchUniverse} diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 298a07c1c4..7022987096 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Arguments ADMIT [p]. +Arguments ADMIT {p}. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/micromega/bug_11191a.v b/test-suite/micromega/bug_11191a.v new file mode 100644 index 0000000000..57c1d7d52f --- /dev/null +++ b/test-suite/micromega/bug_11191a.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p n, (0 < Z.pos (p ^ n))%Z. + intros. + lia. +Qed. diff --git a/test-suite/micromega/bug_11191b.v b/test-suite/micromega/bug_11191b.v new file mode 100644 index 0000000000..007470c5b3 --- /dev/null +++ b/test-suite/micromega/bug_11191b.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p, (0 < Z.pos (p ^ 2))%Z. + intros. + lia. +Qed. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index d293dc0533..048fb3b027 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -65,7 +65,7 @@ Proof. by []. Qed. Lemma eqP T : Equality.axiom (@eq_op T). Proof. by case: T => ? []. Qed. -Arguments eqP [T x y]. +Arguments eqP {T x y}. Delimit Scope eq_scope with EQ. Open Scope eq_scope. @@ -345,7 +345,7 @@ Proof. by []. Qed. End SubEqType. -Arguments val_eqP [T P sT x y]. +Arguments val_eqP {T P sT x y}. Prenex Implicits val_eqP. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) @@ -386,7 +386,7 @@ Qed. Canonical nat_eqMixin := EqMixin eqnP. Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. -Arguments eqnP [x y]. +Arguments eqnP {x y}. Prenex Implicits eqnP. Coercion nat_of_bool (b : bool) := if b then 1 else 0. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index c2130995fc..4b2d4457bf 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Arguments LNil [A]. +Arguments LNil {A}. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil @@ -204,3 +204,19 @@ End NonRecLetIn. Fail Inductive foo (T : Type) : let T := Type in T := { r : forall x : T, x = x }. + +Module Discharge. + (* discharge test *) + Section S. + Let x := Prop. + Inductive foo : x := bla : foo. + End S. + Check bla:foo. + + Section S. + Variables (A:Type). + (* ensure params are scanned for needed section variables even with template arity *) + #[universes(template)] Inductive bar (d:A) := . + End S. + Check @bar nat 0. +End Discharge. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 1dbeaf3e1f..8297f54641 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Arguments NL [I]. +Arguments NL {I}. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 4fac798f76..15672eab7c 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -994,7 +994,7 @@ Qed. Arguments Vector.cons [A] _ [n]. -Arguments Vector.nil [A]. +Arguments Vector.nil {A}. Arguments Vector.hd [A n]. Arguments Vector.tl [A n]. @@ -1161,7 +1161,7 @@ infiniteproof map_iterate'. Qed. -Arguments LNil [A]. +Arguments LNil {A}. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index 855f26698c..4b928007cf 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep. Set Rewriting Schemes. Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. Unset Rewriting Schemes. + +(* check that the scheme doesn't minimize itself into something non general *) +Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . +Lemma bla@{u v|u < v} : foo@{u v} -> False. +Proof. induction 1. Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 28d1c2c97f..332d3b14e4 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -24,7 +24,6 @@ Require Export Rsqrt_def. Require Export R_sqrt. Require Export Rtrigo_calc. Require Export Rgeom. -Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index cb6d57be84..e6b3f2e37b 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -24,7 +24,6 @@ Require Export Rsqrt_def. Require Export R_sqrt. Require Export Rtrigo_calc. Require Export Rgeom. -Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index a848a59d48..0337b12cad 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -15,6 +15,7 @@ Require Import Ranalysis_reg. Require Import Rbase. Require Import RiemannInt_SF. Require Import Max. +Require Import RList. Local Open Scope R_scope. Set Implicit Arguments. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 6da0fe3966..c8ec4782d9 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -12,6 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis_reg. Require Import Classical_Prop. +Require Import RList. Local Open Scope R_scope. Set Implicit Arguments. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5544024993..52e2562ae8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -198,6 +198,14 @@ let set_query opts q = | Queries queries -> Queries (queries@[q]) } +let warn_depr_load_ml_object = + CWarnings.create ~name:"deprecated-mlobject" ~category:"deprecated" + (fun () -> Pp.strbrk "The -load-ml-object option is deprecated, see the changelog for more details.") + +let warn_depr_ml_load_source = + CWarnings.create ~name:"deprecated-mlsource" ~category:"deprecated" + (fun () -> Pp.strbrk "The -load-ml-source option is deprecated, see the changelog for more details.") + let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") @@ -396,9 +404,11 @@ let parse_args ~help ~init arglist : t * string list = set_inputstate oval (next ()) |"-load-ml-object" -> + warn_depr_load_ml_object (); Mltop.dir_ml_load (next ()); oval |"-load-ml-source" -> + warn_depr_ml_load_source (); Mltop.dir_ml_use (next ()); oval |"-load-vernac-object" -> diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 69ba9d76ec..def2fdad2a 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -72,7 +72,7 @@ let declare_univ_binders gr pl = CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") + Pp.(str "declare_univ_binders on a constructor reference") in let univs = Id.Map.fold (fun id univ univs -> match Univ.Level.name univ with diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 222e9eb825..05e23164b1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1346,7 +1346,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:false in + let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e98820bc98..d011fb2e77 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1453,6 +1453,14 @@ let () = optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } +let () = + declare_bool_option + { optdepr = false; + optname = "enable native compute timing"; + optkey = ["NativeCompute"; "Timing"]; + optread = Nativenorm.get_timing_enabled; + optwrite = Nativenorm.set_timing_enabled } + let _ = declare_bool_option { optdepr = false; |