diff options
62 files changed, 677 insertions, 257 deletions
diff --git a/.gitignore b/.gitignore index c30fd850a1..4e02e7617c 100644 --- a/.gitignore +++ b/.gitignore @@ -145,7 +145,9 @@ plugins/ssr/ssrvernac.ml # other auto-generated files +kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +kernel/genOpcodeFiles.exe kernel/copcodes.ml kernel/uint63.ml ide/index_urls.txt diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a1da9be20b..c5038d3bb0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -209,6 +209,17 @@ after_script: variables: - $WINDOWS =~ /enabled/ +.deploy-template: &deploy-template + stage: deploy + before_script: + - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) + - eval $(ssh-agent -s) + - mkdir -p ~/.ssh + - chmod 700 ~/.ssh + - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts + - git config --global user.name "coqbot" + - git config --global user.email "coqbot@users.noreply.github.com" + build:base: <<: *build-template variables: @@ -325,6 +336,21 @@ pkg:nix:deploy: - master - /^v.*\..*$/ +pkg:nix:deploy:channel: + <<: *deploy-template + environment: + name: cachix + url: https://coq.cachix.org + only: + variables: + - $CACHIX_DEPLOYMENT_KEY + dependencies: + - pkg:nix:deploy + script: + - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null + - git fetch --unshallow + - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_REF_NAME}" + pkg:nix: <<: *nix-template except: @@ -357,7 +383,7 @@ doc:stdlib:dune: - _build/default/doc/stdlib/html doc:refman:deploy: - stage: deploy + <<: *deploy-template environment: name: deployment url: https://coq.github.io/ @@ -368,14 +394,6 @@ doc:refman:deploy: - doc:ml-api:odoc - doc:refman:dune - doc:stdlib:dune - before_script: - - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) - - eval $(ssh-agent -s) - - mkdir -p ~/.ssh - - chmod 700 ~/.ssh - - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts - - git config --global user.name "coqbot" - - git config --global user.email "coqbot@users.noreply.github.com" script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy @@ -566,6 +584,9 @@ library:ci-math-comp: library:ci-sf: <<: *ci-template +library:ci-stdlib2: + <<: *ci-template-flambda + library:ci-unimath: <<: *ci-template-flambda diff --git a/CHANGES.md b/CHANGES.md index af2b7991dd..59cc17c233 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -97,6 +97,9 @@ Tactics - Ltac backtraces can be turned on using the "Ltac Backtrace" option. +- The syntax of the `autoapply` tactic was fixed to conform with preexisting + documentation: it now takes a `with` clause instead of a `using` clause. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort @@ -75,16 +75,22 @@ endef ## Files in the source tree +# instead of using "export FOO" do "COQ_EXPORTED += FOO" +# this makes it possible to clean up the environment in the subcall +COQ_EXPORTED := COQ_EXPORTED + LEXFILES := $(call find, '*.mll') YACCFILES := $(call find, '*.mly') -export MLLIBFILES := $(call find, '*.mllib') -export MLPACKFILES := $(call find, '*.mlpack') -export MLGFILES := $(call find, '*.mlg') -export CFILES := $(call findindir, 'kernel/byterun', '*.c') +MLLIBFILES := $(call find, '*.mllib') +MLPACKFILES := $(call find, '*.mlpack') +MLGFILES := $(call find, '*.mlg') +CFILES := $(call findindir, 'kernel/byterun', '*.c') +COQ_EXPORTED +=MLLIBFILES MLPACKFILES MLGFILES CFILES # NB our find wrapper ignores the test suite MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in -export MERLINFILES := $(MERLININFILES:.in=) +MERLINFILES := $(MERLININFILES:.in=) +COQ_EXPORTED += MERLINFILES # NB: The lists of currently existing .ml and .mli files will change # before and after a build or a make clean. Hence we do not export @@ -97,17 +103,21 @@ EXISTINGMLI := $(call find, '*.mli') GENMLGFILES:= $(MLGFILES:.mlg=.ml) # GRAMFILES must be in linking order -export GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) -export GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) -export GENGRAMFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml -export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) +GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) +GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) +GENGRAMFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml +GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) +COQ_EXPORTED += GRAMFILES GRAMMLFILES GENGRAMFILES GENMLFILES GENHFILES GENFILES ## More complex file lists -export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) -export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) +MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) +MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) +COQ_EXPORTED += MLSTATICFILES MLIFILES + +export $(COQ_EXPORTED) include Makefile.common diff --git a/Makefile.build b/Makefile.build index ea356d5f8e..8b989f161a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -11,6 +11,9 @@ # This makefile is normally called by the main Makefile after setting # some variables. +# Cleanup environment (avoids filling it up) +unexport $(COQ_EXPORTED) + ########################################################################### # User-customizable variables ########################################################################### @@ -316,11 +319,21 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN)) -kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h kernel/byterun/make_jumptbl.sh - kernel/byterun/make_jumptbl.sh $< $@ +kernel/genOpcodeFiles.exe: kernel/genOpcodeFiles.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -o $@ $< + +kernel/byterun/coq_instruct.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< enum > $@ -kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/make-opcodes - kernel/make_opcodes.sh $< $@ +kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< jump > $@ + +kernel/copcodes.ml: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< copml > $@ %.o: %.c $(SHOW)'OCAMLC $<' @@ -849,6 +862,18 @@ $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT ########################################################################### + +# Useful to check that the exported variables are within the win32 limits + +printenv-real: + @env + @echo + @echo -n "Maxsize (win32 limit is 8k) : " + @env | wc -L + @echo -n "Total (win32 limit is 32k) : " + @env | wc -m + + # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles Makefile $(wildcard Makefile.*) config/Makefile : ; @@ -863,5 +888,5 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # For emacs: # Local Variables: -# mode: makefile +# mode: makefile-gmake # End: diff --git a/Makefile.ci b/Makefile.ci index 0307d39d54..9180d51bee 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -40,6 +40,7 @@ CI_TARGETS= \ ci-relation-algebra \ ci-sf \ ci-simple-io \ + ci-stdlib2 \ ci-tlc \ ci-unimath \ ci-verdi-raft \ diff --git a/Makefile.dune b/Makefile.dune index da4c59af75..4609c563d9 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -3,7 +3,7 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets -.PHONY: quickbyte quickopt # Partial / quick developer targets +.PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accesory targets .PHONY: ocheck trunk ireport clean # Maintenance targets @@ -27,6 +27,7 @@ help: @echo "" @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" + @echo " - quickide: build main IDE files [client + server + prelude] using the optimizing compiler" @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" @@ -40,12 +41,14 @@ help: @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" +# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work. voboot: + @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune dune build $(DUNEOPT) @vodeps dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d states: voboot - dune build $(DUNEOPT) theories/Init/Prelude.vo + dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude world: voboot dune build $(DUNEOPT) @install @@ -77,6 +80,9 @@ quickbyte: voboot quickopt: voboot dune build $(DUNEOPT) $(QUICKOPT_TARGETS) +quickide: states + dune build $(DUNEOPT) dev/shim/coqide-prelude + test-suite: voboot dune runtest --no-buffer $(DUNEOPT) diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4329b2d743..b681fb876e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -89,6 +89,9 @@ let eq_recarg a1 a2 = match a1, a2 with let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) +let eq_in_context (ctx1, t1) (ctx2, t2) = + Context.Rel.equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2 + let check_packet env mind ind { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; @@ -105,7 +108,7 @@ let check_packet env mind ind check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); - check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); + check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also care about the shape of the terms *) diff --git a/checker/values.ml b/checker/values.ml index 66467fa8f5..bcac3014be 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -261,7 +261,7 @@ let v_one_ind = v_tuple "one_inductive_body" Int; Int; List v_sortfam; - Array v_constr; + Array (v_pair v_rctxt v_constr); Array Int; Array Int; v_wfp; diff --git a/clib/cMap.ml b/clib/cMap.ml index e4ce6c7c02..016d8bdeca 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -36,6 +36,7 @@ sig val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val height : 'a t -> int val filter_range : (key -> int) -> 'a t -> 'a t + val update: key -> ('a option -> 'a option) -> 'a t -> 'a t module Smart : sig val map : ('a -> 'a) -> 'a t -> 'a t @@ -64,6 +65,7 @@ sig val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val height : 'a map -> int val filter_range : (M.t -> int) -> 'a map -> 'a map + val update: M.t -> ('a option -> 'a option) -> 'a map -> 'a map module Smart : sig val map : ('a -> 'a) -> 'a map -> 'a map @@ -94,8 +96,8 @@ struct type set = S.t type 'a _map = - | MEmpty - | MNode of 'a map * M.t * 'a * 'a map * int + | MEmpty + | MNode of {l:'a map; v:F.key; d:'a; r:'a map; h:int} type _set = | SEmpty @@ -108,41 +110,41 @@ struct let rec set k v (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found - | MNode (l, k', v', r, h) -> + | MNode {l; v=k'; d=v'; r; h} -> let c = M.compare k k' in if c < 0 then let l' = set k v l in if l == l' then s - else map_inj (MNode (l', k', v', r, h)) + else map_inj (MNode {l=l'; v=k'; d=v'; r; h}) else if c = 0 then if v' == v then s - else map_inj (MNode (l, k', v, r, h)) + else map_inj (MNode {l; v=k'; d=v; r; h}) else let r' = set k v r in if r == r' then s - else map_inj (MNode (l, k', v', r', h)) + else map_inj (MNode {l; v=k'; d=v'; r=r'; h}) let rec modify k f (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found - | MNode (l, k', v, r, h) -> - let c = M.compare k k' in + | MNode {l; v; d; r; h} -> + let c = M.compare k v in if c < 0 then let l' = modify k f l in if l == l' then s - else map_inj (MNode (l', k', v, r, h)) + else map_inj (MNode {l=l'; v; d; r; h}) else if c = 0 then - let v' = f k' v in - if v' == v then s - else map_inj (MNode (l, k', v', r, h)) + let d' = f v d in + if d' == d then s + else map_inj (MNode {l; v; d=d'; r; h}) else let r' = modify k f r in if r == r' then s - else map_inj (MNode (l, k', v, r', h)) + else map_inj (MNode {l; v; d; r=r'; h}) let rec domain (s : 'a map) : set = match map_prj s with | MEmpty -> set_inj SEmpty - | MNode (l, k, _, r, h) -> - set_inj (SNode (domain l, k, domain r, h)) + | MNode {l; v; r; h; _} -> + set_inj (SNode (domain l, v, domain r, h)) (** This function is essentially identity, but OCaml current stdlib does not take advantage of the similarity of the two structures, so we introduce this unsafe loophole. *) @@ -150,31 +152,31 @@ struct let rec bind f (s : set) : 'a map = match set_prj s with | SEmpty -> map_inj MEmpty | SNode (l, k, r, h) -> - map_inj (MNode (bind f l, k, f k, bind f r, h)) + map_inj (MNode { l=bind f l; v=k; d=f k; r=bind f r; h}) (** Dual operation of [domain]. *) let rec fold_left f (s : 'a map) accu = match map_prj s with | MEmpty -> accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let accu = f k v (fold_left f l accu) in fold_left f r accu let rec fold_right f (s : 'a map) accu = match map_prj s with | MEmpty -> accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let accu = f k v (fold_right f r accu) in fold_right f l accu let height s = match map_prj s with | MEmpty -> 0 - | MNode (_, _, _, _, h) -> h + | MNode {h;_} -> h (* Filter based on a range *) let filter_range in_range m = let rec aux m = function | MEmpty -> m - | MNode (l, k, v, r, _) -> - let vr = in_range k in + | MNode {l; v; d; r; _} -> + let vr = in_range v in (* the range is below the current value *) if vr < 0 then aux m (map_prj l) (* the range is above the current value *) @@ -183,29 +185,102 @@ struct else let m = aux m (map_prj l) in let m = aux m (map_prj r) in - F.add k v m + F.add v d m in aux F.empty (map_prj m) + (* Imported from OCaml upstream until we can bump the version *) + let create l x d r = + let hl = height l and hr = height r in + map_inj @@ MNode{l; v=x; d; r; h=(if hl >= hr then hl + 1 else hr + 1)} + + let bal l x d r = + let hl = match map_prj l with MEmpty -> 0 | MNode {h} -> h in + let hr = match map_prj r with MEmpty -> 0 | MNode {h} -> h in + if hl > hr + 2 then begin + match map_prj l with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=ll; v=lv; d=ld; r=lr} -> + if height ll >= height lr then + create ll lv ld (create lr x d r) + else begin + match map_prj lr with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=lrl; v=lrv; d=lrd; r=lrr}-> + create (create ll lv ld lrl) lrv lrd (create lrr x d r) + end + end else if hr > hl + 2 then begin + match map_prj r with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=rl; v=rv; d=rd; r=rr} -> + if height rr >= height rl then + create (create l x d rl) rv rd rr + else begin + match map_prj rl with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=rll; v=rlv; d=rld; r=rlr} -> + create (create l x d rll) rlv rld (create rlr rv rd rr) + end + end else + map_inj @@ MNode{l; v=x; d; r; h=(if hl >= hr then hl + 1 else hr + 1)} + + let rec remove_min_binding m = match map_prj m with + | MEmpty -> invalid_arg "Map.remove_min_elt" + | MNode {l;v;d;r;_} -> + match map_prj l with + | MEmpty -> r + | _ -> bal (remove_min_binding l) v d r + + let merge t1 t2 = + match (map_prj t1, map_prj t2) with + (MEmpty, t) -> map_inj t + | (t, MEmpty) -> map_inj t + | (_, _) -> + let (x, d) = F.min_binding t2 in + bal t1 x d (remove_min_binding t2) + + let rec update x f m = match map_prj m with + | MEmpty -> + begin match f None with + | None -> map_inj MEmpty + | Some data -> map_inj @@ MNode{l=map_inj MEmpty; v=x; d=data; r=map_inj MEmpty; h=1} + end + | MNode {l; v; d; r; h} as m -> + let c = M.compare x v in + if c = 0 then begin + match f (Some d) with + | None -> merge l r + | Some data -> + if d == data then map_inj m else + map_inj @@ MNode{l; v=x; d=data; r; h} + end else if c < 0 then + let ll = update x f l in + if l == ll then map_inj m else bal ll v d r + else + let rr = update x f r in + if r == rr then map_inj m else bal l v d rr + + (* End of Imported OCaml *) + module Smart = struct let rec map f (s : 'a map) = match map_prj s with | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let l' = map f l in let r' = map f r in let v' = f v in if l == l' && r == r' && v == v' then s - else map_inj (MNode (l', k, v', r', h)) + else map_inj (MNode {l=l'; v=k; d=v'; r=r'; h}) let rec mapi f (s : 'a map) = match map_prj s with | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let l' = mapi f l in let r' = mapi f r in let v' = f k v in if l == l' && r == r' && v == v' then s - else map_inj (MNode (l', k, v', r', h)) + else map_inj (MNode {l=l'; v=k; d=v'; r=r'; h}) end @@ -214,9 +289,9 @@ struct let rec map f (s : 'a map) : 'b map = match map_prj s with | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let (k, v) = f k v in - map_inj (MNode (map f l, k, v, map f r, h)) + map_inj (MNode {l=map f l; v=k; d=v; r=map f r; h}) end @@ -227,14 +302,14 @@ struct let rec fold_left f s accu = match map_prj s with | MEmpty -> return accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> fold_left f l accu >>= fun accu -> f k v accu >>= fun accu -> fold_left f r accu let rec fold_right f s accu = match map_prj s with | MEmpty -> return accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> fold_right f r accu >>= fun accu -> f k v accu >>= fun accu -> fold_right f l accu diff --git a/clib/cMap.mli b/clib/cMap.mli index ca6ddb2f4e..9bbb8d50dd 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -66,6 +66,18 @@ sig [filter_range] returns the submap of [m] whose keys are in range. Note that [in_range] has to define a continouous range. *) + val update: key -> ('a option -> 'a option) -> 'a t -> 'a t + (** [update x f m] returns a map containing the same bindings as + [m], except for the binding of [x]. Depending on the value of + [y] where [y] is [f (find_opt x m)], the binding of [x] is + added, removed or updated. If [y] is [None], the binding is + removed if it exists; otherwise, if [y] is [Some z] then [x] + is associated to [z] in the resulting map. If [x] was already + bound in [m] to a value that is physically equal to [z], [m] + is returned unchanged (the result of the function is then + physically equal to [m]). + *) + module Smart : sig val map : ('a -> 'a) -> 'a t -> 'a t diff --git a/clib/hMap.ml b/clib/hMap.ml index 5d634b7af0..09ffb39c21 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -408,6 +408,18 @@ struct let filter_range f s = filter (fun x _ -> f x = 0) s + let update k f m = + let aux = function + | None -> (match f None with + | None -> None + | Some v -> Some (Map.singleton k v)) + | Some m -> + let m = Map.update k f m in + if Map.is_empty m then None + else Some m + in + Int.Map.update (M.hash k) aux m + module Unsafe = struct let map f s = diff --git a/default.nix b/default.nix index b65d736d79..3290f5dee8 100644 --- a/default.nix +++ b/default.nix @@ -78,7 +78,6 @@ stdenv.mkDerivation rec { !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; preConfigure = '' - patchShebangs kernel/ patchShebangs dev/tools/ ''; diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 74e8d3bbaa..deeec3942d 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -289,3 +289,10 @@ : "${verdi_raft_CI_REF:=master}" : "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" : "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" + +######################################################################## +# stdlib2 +######################################################################## +: "${stdlib2_CI_REF:=master}" +: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" +: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh new file mode 100755 index 0000000000..ec1c180d7d --- /dev/null +++ b/dev/ci/ci-stdlib2.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download stdlib2 + +( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install) diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh new file mode 100644 index 0000000000..1af8b5430d --- /dev/null +++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then + + quickchick_CI_REF=context-constructor + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + equations_CI_REF=context-constructor + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 5705857d76..3f1b470878 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -37,6 +37,9 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. +To know what files you are a code owner of in a large PR, you can run +`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect. + When a PR received lots of comments or if the PR has not been opened for long and the assignee thinks that some other developers might want to comment, it is recommended that they announce their intention to merge and wait a full diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index da91c85856..a31ab1c511 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -44,6 +44,24 @@ Dune will read the file `~/.config/dune/config`; see `man dune-config`. Among others, you can set in this file the custom number of build threads `(jobs N)` and display options `(display _mode_)`. +## Running binaries [coqtop / coqide] + +There are two special targets `states` and `quickide` that will +generate "shims" for running `coqtop` and `coqide` in a fast build. In +order to use them, do: + +``` +$ make -f Makefile.dune voboot # Only once per session +$ dune exec dev/shim/coqtop-prelude +``` + +or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets +enjoy quick incremental compilation thanks to `-opaque` so they tend +to be very fast while developing. + +Note that for a fast developer build of ML files, the `check` target +will be faster. + ## Targets The default dune target is `dune build` (or `dune build @install`), diff --git a/dev/shim/dune b/dev/shim/dune new file mode 100644 index 0000000000..85a0d205da --- /dev/null +++ b/dev/shim/dune @@ -0,0 +1,27 @@ +(rule + (targets coqtop-prelude) + (deps + %{bin:coqtop} + %{project_root}/theories/Init/Prelude.vo) + (action + (with-outputs-to coqtop-prelude + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) + +(rule + (targets coqide-prelude) + (deps + %{bin:coqqueryworker.opt} + %{bin:coqtacticworker.opt} + %{bin:coqproofworker.opt} + %{project_root}/theories/Init/Prelude.vo + %{project_root}/coqide-server.install + %{project_root}/coqide.install) + (action + (with-outputs-to coqide-prelude + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index ec72f96509..c6687b9731 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -80,9 +80,8 @@ Note that this function is executed before _Coqproject is read if it exists." (when dir (unless coq-prog-args (setq coq-prog-args - `("-coqlib" ,dir "-R" ,(concat dir "plugins") - "Coq" "-R" ,(concat dir "theories") - "Coq"))) + `("-coqlib" ,dir + "-topfile" ,buffer-file-name))) (setq-local coq-prog-name (concat dir "bin/coqtop"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 237b534d67..b81830f06b 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2094,9 +2094,9 @@ into a closing one (similar to :tacn:`now`). Its general syntax is: :name: by :undocumented: -The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to -:n:`[by @tactic | by @tactic | ...]` and this form should be preferred -to the former. +The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to +:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the +standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 24894fc9f5..7f1dc70d95 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1188,7 +1188,6 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr))) -open Term open Declarations (* Similar to Cases.adjust_local_defs but on RCPat *) @@ -1197,16 +1196,15 @@ let insert_local_defs_in_pattern (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in - let (decls,_) = decompose_prod_assum typi in + let (ctx, _) = mip.mind_nf_lc.(j-1) in + let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in let rec aux decls args = match decls, args with | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) l + aux decls l let add_local_defs_and_check_length loc env g pl args = match g with | ConstructRef cstr -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 6fd52d98dd..2c281af2d2 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -452,9 +452,10 @@ let compute_mib_implicits flags kn = let ind = (kn,i) in let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), - Array.mapi (fun j c -> + Array.mapi (fun j (ctx, cty) -> + let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) - (Array.map of_constr mip.mind_nf_lc)) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h deleted file mode 100644 index c7abedaed6..0000000000 --- a/kernel/byterun/coq_instruct.h +++ /dev/null @@ -1,67 +0,0 @@ -/***********************************************************************/ -/* */ -/* Coq Compiler */ -/* */ -/* Benjamin Gregoire, projets Logical and Cristal */ -/* INRIA Rocquencourt */ -/* */ -/* */ -/***********************************************************************/ - -#ifndef _COQ_INSTRUCT_ -#define _COQ_INSTRUCT_ - -/* Nota: this list of instructions is parsed to produce derived files */ -/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ -/* and alone on lines starting by two spaces. */ -/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ -/* with the arity of the instruction and maybe coq_tcode_of_code. */ - -enum instructions { - ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, - PUSH, - PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4, - PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, - POP, - ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC, - PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC, - PUSH_RETADDR, - APPLY, APPLY1, APPLY2, APPLY3, APPLY4, - APPTERM, APPTERM1, APPTERM2, APPTERM3, - RETURN, RESTART, GRAB, GRABREC, - CLOSURE, CLOSUREREC, CLOSURECOFIX, - OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE, - PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, - PUSHOFFSETCLOSURE, - GETGLOBAL, PUSHGETGLOBAL, - MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4, - SWITCH, PUSHFIELDS, - GETFIELD0, GETFIELD1, GETFIELD, - SETFIELD0, SETFIELD1, SETFIELD, - PROJ, - ENSURESTACKCAPACITY, - CONST0, CONST1, CONST2, CONST3, CONSTINT, - PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, - MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, -/* spiwack: */ - BRANCH, - CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63, - CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63, - CHECKMULINT63, CHECKMULCINT63, - CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63, - CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63, - CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63, - CHECKLSLINT63CONST1, CHECKLSRINT63CONST1, - - CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63, - CHECKCOMPAREINT63, - - CHECKHEAD0INT63, CHECKTAIL0INT63, - - ISINT, AREINT2, - - STOP -}; - -#endif /* _COQ_INSTRUCT_ */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index c3c44670be..20bdf28e54 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -5,6 +5,9 @@ (c_names coq_fix_code coq_memory coq_values coq_interp)) (rule + (targets coq_instruct.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum)))) + +(rule (targets coq_jumptbl.h) - (deps (:h-file coq_instruct.h) make_jumptbl.sh) - (action (bash "./make_jumptbl.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh deleted file mode 100755 index eacd4daac8..0000000000 --- a/kernel/byterun/make_jumptbl.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/usr/bin/env bash - -sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2} diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 6777e0c223..567850645e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -166,7 +166,7 @@ type one_inductive_body = { mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) - mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) + mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; (** Number of expected proper arguments of the constructors (w/o params) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 9e0230c3ba..d56502a095 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -214,7 +214,7 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (fun (ctx, c) -> Context.Rel.map (subst_mps sub) ctx, subst_mps sub c) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; @@ -299,9 +299,8 @@ let hcons_ind_arity = let hcons_mind_packet oib = let user = Array.Smart.map Constr.hcons oib.mind_user_lc in - let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in - (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) - let nf = if Array.equal (==) user nf then user else nf in + let map (ctx, c) = Context.Rel.map Constr.hcons ctx, Constr.hcons c in + let nf = Array.Smart.map map oib.mind_nf_lc in { oib with mind_typename = Names.Id.hcons oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; diff --git a/kernel/dune b/kernel/dune index 1f2d696a36..a8a87a3e95 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,13 +3,16 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) (libraries lib byterun)) +(executable + (name genOpcodeFiles) + (modules genOpcodeFiles)) + (rule (targets copcodes.ml) - (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh) - (action (bash "./make_opcodes.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) (executable (name write_uint63) diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml new file mode 100644 index 0000000000..6564954dfd --- /dev/null +++ b/kernel/genOpcodeFiles.ml @@ -0,0 +1,193 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** List of opcodes. + + It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and + [copcodes.ml] files. + + If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c + with the arity of the instruction and maybe coq_tcode_of_code. +*) +let opcodes = + [| + "ACC0"; + "ACC1"; + "ACC2"; + "ACC3"; + "ACC4"; + "ACC5"; + "ACC6"; + "ACC7"; + "ACC"; + "PUSH"; + "PUSHACC0"; + "PUSHACC1"; + "PUSHACC2"; + "PUSHACC3"; + "PUSHACC4"; + "PUSHACC5"; + "PUSHACC6"; + "PUSHACC7"; + "PUSHACC"; + "POP"; + "ENVACC1"; + "ENVACC2"; + "ENVACC3"; + "ENVACC4"; + "ENVACC"; + "PUSHENVACC1"; + "PUSHENVACC2"; + "PUSHENVACC3"; + "PUSHENVACC4"; + "PUSHENVACC"; + "PUSH_RETADDR"; + "APPLY"; + "APPLY1"; + "APPLY2"; + "APPLY3"; + "APPLY4"; + "APPTERM"; + "APPTERM1"; + "APPTERM2"; + "APPTERM3"; + "RETURN"; + "RESTART"; + "GRAB"; + "GRABREC"; + "CLOSURE"; + "CLOSUREREC"; + "CLOSURECOFIX"; + "OFFSETCLOSUREM2"; + "OFFSETCLOSURE0"; + "OFFSETCLOSURE2"; + "OFFSETCLOSURE"; + "PUSHOFFSETCLOSUREM2"; + "PUSHOFFSETCLOSURE0"; + "PUSHOFFSETCLOSURE2"; + "PUSHOFFSETCLOSURE"; + "GETGLOBAL"; + "PUSHGETGLOBAL"; + "MAKEBLOCK"; + "MAKEBLOCK1"; + "MAKEBLOCK2"; + "MAKEBLOCK3"; + "MAKEBLOCK4"; + "SWITCH"; + "PUSHFIELDS"; + "GETFIELD0"; + "GETFIELD1"; + "GETFIELD"; + "SETFIELD0"; + "SETFIELD1"; + "SETFIELD"; + "PROJ"; + "ENSURESTACKCAPACITY"; + "CONST0"; + "CONST1"; + "CONST2"; + "CONST3"; + "CONSTINT"; + "PUSHCONST0"; + "PUSHCONST1"; + "PUSHCONST2"; + "PUSHCONST3"; + "PUSHCONSTINT"; + "ACCUMULATE"; + "MAKESWITCHBLOCK"; + "MAKEACCU"; + "MAKEPROD"; + "BRANCH"; + "CHECKADDINT63"; + "ADDINT63"; + "CHECKADDCINT63"; + "CHECKADDCARRYCINT63"; + "CHECKSUBINT63"; + "SUBINT63"; + "CHECKSUBCINT63"; + "CHECKSUBCARRYCINT63"; + "CHECKMULINT63"; + "CHECKMULCINT63"; + "CHECKDIVINT63"; + "CHECKMODINT63"; + "CHECKDIVEUCLINT63"; + "CHECKDIV21INT63"; + "CHECKLXORINT63"; + "CHECKLORINT63"; + "CHECKLANDINT63"; + "CHECKLSLINT63"; + "CHECKLSRINT63"; + "CHECKADDMULDIVINT63"; + "CHECKLSLINT63CONST1"; + "CHECKLSRINT63CONST1"; + "CHECKEQINT63"; + "CHECKLTINT63"; + "LTINT63"; + "CHECKLEINT63"; + "LEINT63"; + "CHECKCOMPAREINT63"; + "CHECKHEAD0INT63"; + "CHECKTAIL0INT63"; + "ISINT"; + "AREINT2"; + "STOP" + |] + +let pp_c_comment fmt = + Format.fprintf fmt "/* %a */" + +let pp_ocaml_comment fmt = + Format.fprintf fmt "(* %a *)" + +let pp_header isOcaml fmt = + Format.fprintf fmt "%a" + (fun fmt -> + (if isOcaml then pp_ocaml_comment else pp_c_comment) fmt + Format.pp_print_string) + "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml" + +let pp_with_commas fmt k = + Array.iteri (fun n s -> + Format.fprintf fmt " %a%s@." + k s + (if n + 1 < Array.length opcodes + then "," else "") + ) opcodes + +let pp_coq_instruct_h fmt = + let line = Format.fprintf fmt "%s@." in + pp_header false fmt; + line "#pragma once"; + line "enum instructions {"; + pp_with_commas fmt Format.pp_print_string; + line "};" + +let pp_coq_jumptbl_h fmt = + pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s") + +let pp_copcodes_ml fmt = + pp_header true fmt; + Array.iteri (fun n s -> + Format.fprintf fmt "let op%s = %d@.@." s n + ) opcodes + +let usage () = + Format.eprintf "usage: %s [enum|jump|copml]@." Sys.argv.(0); + exit 1 + +let main () = + match Sys.argv.(1) with + | "enum" -> pp_coq_instruct_h Format.std_formatter + | "jump" -> pp_coq_jumptbl_h Format.std_formatter + | "copml" -> pp_copcodes_ml Format.std_formatter + | _ -> usage () + | exception Invalid_argument _ -> usage () + +let () = main () diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8f06e1e4b8..457c17907e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -416,7 +416,9 @@ let compute_projections (kn, i as ind) mib = let pkt = mib.mind_packets.(i) in let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let (ctx, cty) = pkt.mind_nf_lc.(0) in + let cty = it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (substl subst cty) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -475,7 +477,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (* Check one inductive *) let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = (* Type of constructors in normal form *) - let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in + let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in let consnrealdecls = Array.map (fun (d,_) -> Context.Rel.length d) splayed_lc in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 848ae65c51..f4c2483c14 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -251,7 +251,11 @@ let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - Array.map (constructor_instantiate kn u mib) specif + let map (ctx, c) = + let cty = Term.it_mkProd_or_LetIn c ctx in + constructor_instantiate kn u mib cty + in + Array.map map specif let arities_of_constructors ind specif = arities_of_specif (fst (fst ind), snd ind) specif @@ -342,7 +346,8 @@ let is_correct_arity env c pj ind specif params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) let build_branches_type (ind,u) (_,mip as specif) params p = - let build_one_branch i cty = + let build_one_branch i (ctx, c) = + let cty = Term.it_mkProd_or_LetIn c ctx in let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (cstrsign,ccl) = Term.decompose_prod_assum typi in let nargs = Context.Rel.length cstrsign in @@ -597,6 +602,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc ntyps npars lc = + let lc = Array.map (fun (ctx, c) -> Term.it_mkProd_or_LetIn c ctx) lc in if Int.equal npars 0 then lc else diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 3c1464c6c9..ad35c16c22 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec val lambda_implicit_lift : int -> constr -> constr -val abstract_mind_lc : int -> Int.t -> constr array -> constr array +val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array diff --git a/kernel/make-opcodes b/kernel/make-opcodes deleted file mode 100644 index e1371b3d0c..0000000000 --- a/kernel/make-opcodes +++ /dev/null @@ -1,3 +0,0 @@ -$1=="enum" {n=0; next; } - {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); - for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh deleted file mode 100755 index bb8aba2f07..0000000000 --- a/kernel/make_opcodes.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash - -script_dir="$(dirname "$0")" -tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | awk -f "$script_dir"/make-opcodes > "${2}" diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index 0fcaf4f10a..beb59ce205 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -1,10 +1,18 @@ -(** Equivalent of rm -f *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(** Equivalent of rm -f *) let safe_remove f = try Unix.chmod f 0o644; Sys.remove f with _ -> () (** * Generate an implementation of 63-bit arithmetic *) - let ml_file_copy input output = safe_remove output; let i = open_in input in diff --git a/lib/flags.ml b/lib/flags.ml index 1195b8caf1..6718e7a954 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -43,8 +43,6 @@ let with_options ol f x = let record_aux_file = ref false -let test_mode = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 2b4446a1db..bf8846417b 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -35,10 +35,6 @@ be eventually removed by cleanups such as PR#1103 *) val record_aux_file : bool ref -(* Flag set when the test-suite is called. Its only effect to display - verbose information for `Fail` *) -val test_mode : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool diff --git a/lib/future.ml b/lib/future.ml index b372bedc5d..6e7c6fd9e3 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -33,7 +33,7 @@ let _ = CErrors.register_handler (function | _ -> raise CErrors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn -let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x +let id x = x module UUID = struct type t = int diff --git a/library/global.mli b/library/global.mli index 4e2ad92717..afb017a905 100644 --- a/library/global.mli +++ b/library/global.mli @@ -134,7 +134,7 @@ val constr_of_global_in_context : Environ.env -> val type_of_global_in_context : Environ.env -> GlobRef.t -> Constr.types * Univ.AUContext.t - [@@ocaml.deprecated "alias of [Typeops.type_of_global]"] + [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"] (** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : GlobRef.t -> Univ.AUContext.t diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 204f889f90..ef6c07bff2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1044,7 +1044,9 @@ let fake_match_projection env p = let indu = mkIndU (ind,u) in let ctx, paramslet = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + let (ctx, cty) = mip.mind_nf_lc.(0) in + let cty = Term.it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in List.chop mip.mind_consnrealdecls.(0) rctx in let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index a60a966cec..56b3dc97cf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -13,7 +13,6 @@ open Names open Constr open EConstr open Vars -open Termops open Util open Declarations open Globnames @@ -100,9 +99,8 @@ let kind_of_formula env sigma term = else let has_realargs=(n>0) in let is_trivial= - let is_constant c = - Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - Array.exists is_constant mip.mind_nf_lc in + let is_constant n = Int.equal n 0 in + Array.exists is_constant mip.mind_consnrealargs in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 9ecc36bdf3..3f2fabeeee 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -99,8 +99,19 @@ TACTIC EXTEND is_ground | [ "is_ground" constr(ty) ] -> { is_ground ty } END +{ +let deprecated_autoapply_using = + CWarnings.create + ~name:"autoapply-using" ~category:"deprecated" + (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.") +} + TACTIC EXTEND autoapply -| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } +| [ "autoapply" constr(c) "using" preident(i) ] -> { + deprecated_autoapply_using (); + autoapply c i + } +| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i } END { diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a0b1d784f1..7216849948 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let mind,indb = Inductive.lookup_mind_specif env (kn,i) in let tys = indb.Declarations.mind_nf_lc in let renamed_tys = - Array.mapi (fun j t -> + Array.mapi (fun j (ctx, cty) -> + let t = Term.it_mkProd_or_LetIn cty ctx in ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ed7c3d6770..1ad90b2953 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -426,7 +426,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in (match find_row_ind tm1 with | None -> sigma, (current, tmtyp) - | Some (_,(ind,_)) -> + | Some (loc,(ind,_)) -> let sigma, indt = inductive_template !!(pb.env) sigma None ind in let sigma, current = if List.is_empty deps && isEvar sigma typ then @@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | None -> sigma, current | Some sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 68626597fc..affed5389f 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -514,12 +514,11 @@ let rec cases_pattern_of_glob_constr na c = ) c open Declarations -open Term open Context (* Keep only patterns which are not bound to a local definitions *) -let drop_local_defs typi args = - let (decls,_) = decompose_prod_assum typi in +let drop_local_defs params decls args = + let decls = List.skipn (Rel.length params) (List.rev decls) in let rec aux decls args = match decls, args with | [], [] -> [] @@ -531,7 +530,7 @@ let drop_local_defs typi args = end | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) args + aux decls args let add_patterns_for_params_remove_local_defs (ind,j) l = let (mib,mip) = Global.lookup_inductive ind in @@ -540,9 +539,8 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in - drop_local_defs typi l in + let (ctx, _) = mip.mind_nf_lc.(j - 1) in + drop_local_defs mib.mind_params_ctxt ctx l in Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l let add_alias ?loc na c = diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4c02dc0f09..d937456bcb 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -101,7 +101,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); - substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) + let (ctx, cty) = specif.(j - 1) in + substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx)) (* Number of constructors *) @@ -280,8 +281,7 @@ let make_case_info env ind style = let ind_tags = Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = - Array.map2 (fun c n -> - let d,_ = decompose_prod_assum c in + Array.map2 (fun (d, _) n -> Context.Rel.to_tags (List.firstn n d)) mip.mind_nf_lc mip.mind_consnrealdecls in let print_info = { ind_tags; cstr_tags; style } in @@ -462,7 +462,8 @@ let compute_projections env (kn, i as ind) = let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let ctx, cty = pkt.mind_nf_lc.(0) in + let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (* We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -622,9 +623,7 @@ let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map - (fun c -> - Context.Rel.length ((prod_assum c)) - - mib.mind_nparams) + (fun (d, _) -> List.length d - mib.mind_nparams) mip.mind_nf_lc in Array.map2 (set_names env sigma) arities brv diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index b7090e69da..77ae09ee6f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -107,7 +107,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let nparams = Array.length params in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 083661a64b..ff528bd2cf 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -61,7 +61,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in diff --git a/stm/stm.ml b/stm/stm.ml index 8af1a2ebd2..ab388977a5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -3205,10 +3205,9 @@ let edit_at ~doc id = let vcs = VCS.backup () in let on_cur_branch id = let rec aux cur = - if id = cur then true - else match VCS.visit cur with + match VCS.visit cur with | { step = `Fork _ } -> false - | { next } -> aux next in + | { next } -> if id = cur then true else aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in let rec is_pure_aux id = let view = VCS.visit id in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b12018cd66..3c1115d056 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -138,7 +138,7 @@ let get_sym_eq_data env (ind,u) = let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; (* This can be relaxed... *) @@ -173,7 +173,7 @@ let get_non_sym_eq_data env (ind,u) = let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported"; - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; @@ -776,7 +776,7 @@ let build_congr env (eq,refl,ctx) ind = error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 708412720a..395b4928ce 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -106,22 +106,24 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = && (Int.equal mip.mind_nrealargs 0) then if is_strict_conjunction style (* strict conjunction *) then - let ctx = - (prod_assum sigma (snd - (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in + let (ctx, _) = mip.mind_nf_lc.(0) in + let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in if + (* Constructor has a type of the form + c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **) List.for_all (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && - isRel sigma c && - Int.equal (destRel sigma c) mib.mind_nparams) ctx + Constr.isRel c && + Int.equal (Constr.destRel c) mib.mind_nparams) ctx then Some (hdapp,args) else None else + let ctx, cty = mip.mind_nf_lc.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in let ctyp = whd_beta_prod sigma - (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) - (EConstr.of_constr mip.mind_nf_lc.(0)) args) in + (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) @@ -165,12 +167,13 @@ let is_tuple sigma t = it is strict if it has the form "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *) -let test_strict_disjunction n lc = - let open Term in - Array.for_all_i (fun i c -> - match (prod_assum (snd (decompose_prod_n_assum n c))) with - | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) - | _ -> false) 0 lc +let test_strict_disjunction (mib, mip) = + let n = List.length mib.mind_params_ctxt in + let check i (ctx, _) = match List.skipn n (List.rev ctx) with + | [LocalAssum (_, c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) + | _ -> false + in + Array.for_all_i check 0 mip.mind_nf_lc let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = let (hdapp,args) = decompose_app sigma t in @@ -183,14 +186,16 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = && (Int.equal mip.mind_nrealargs 0) then if strict then - if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then + if test_strict_disjunction (mib, mip) then Some (hdapp,args) else None else - let cargs = - Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args))) - mip.mind_nf_lc in + let map (ctx, cty) = + let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + pi2 (destProd sigma (prod_applist sigma ar args)) + in + let cargs = Array.map map mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) else None @@ -225,10 +230,8 @@ let match_with_unit_or_eq_type sigma t = match EConstr.kind sigma hdapp with | Ind (ind , _) -> let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in - let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - if Int.equal nconstr 1 && zero_args constr_types.(0) then + if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then Some hdapp else None @@ -308,11 +311,13 @@ let match_with_equation env sigma t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then - if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then + let (ctx, cty) = constr_types.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + if is_matching env sigma coq_refl_leibniz1_pattern cty then None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_leibniz2_pattern cty then None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_jm_pattern cty then None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else raise NoEquationFound else raise NoEquationFound @@ -378,8 +383,9 @@ let match_with_nodep_ind sigma t = | Ind (ind, _) -> let (mib,mip) = Global.lookup_inductive ind in if Array.length (mib.mind_packets)>1 then None else - let nodep_constr c = - has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in + let nodep_constr (ctx, cty) = + let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -400,7 +406,7 @@ let match_with_sigma_type sigma t = && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma - (EConstr.of_constr mip.mind_nf_lc.(0)) + (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx)) then (*allowing only 1 existential*) Some (hdapp,args) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bfbce8f6eb..ec8d4d0e14 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -20,6 +20,7 @@ open Tacmach open Clenv open Tactypes +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (************************************************************************) @@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = - match Constr.kind c, recargs with - | Prod (_,_,c), recarg::rest -> + match c, recargs with + | RelDecl.LocalAssum _ :: c, recarg::rest -> let rest = analrec c rest in begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest @@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end - | LetIn (_,_,_,c), rest -> false :: analrec c rest - | _, [] -> [] + | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest + | [], [] -> [] | _ -> anomaly (Pp.str "compute_constructor_signatures.") in let (mib,mip) = Global.lookup_inductive ity in - let n = mib.mind_nparams in - let lc = - Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in + let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in + let lc = Array.map map mip.mind_nf_lc in let lrecargs = Declareops.dest_subterms mip.mind_recargs in Array.map2 analrec lc lrecargs diff --git a/test-suite/Makefile b/test-suite/Makefile index 5582503d89..6efd47afc2 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -38,9 +38,9 @@ include ../Makefile.common BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= +COQLIB?= ifeq ($(COQLIB),) - # This method of setting `pwd` won't work on win32 OCaml - COQLIB := $(shell cd ..; pwd) + COQLIB := $(shell ocaml ocaml_pwd.ml ..) endif export COQLIB diff --git a/test-suite/dune b/test-suite/dune index 9efc1e2dc1..c430400ba5 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -6,7 +6,7 @@ (rule (targets libpath.inc) - (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe ../../install/%{context_name}/lib/coq/ )))) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ )))) (rule (targets summary.log) diff --git a/test-suite/ide/reopen1.fake b/test-suite/ide/reopen1.fake new file mode 100644 index 0000000000..2c4f13de86 --- /dev/null +++ b/test-suite/ide/reopen1.fake @@ -0,0 +1,22 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping outside the focused zone should signal an unfocus. + +# first proof +ADD here { Goal True. } +ADD here1 { Proof. } +ADD { Qed. } +WAIT +EDIT_AT here1 +EDIT_AT here +# fwd again +ADD here2 { Proof. } +ADD here3 { Qed. } +WAIT +EDIT_AT here2 +# Fixing the proof +ADD { Proof. } +ADD { trivial. } +ADD { Qed. } +JOIN diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml index 10ca52a4a9..afa3deea3a 100644 --- a/test-suite/ocaml_pwd.ml +++ b/test-suite/ocaml_pwd.ml @@ -1,7 +1,7 @@ let _ = - let ch_dir = Sys.argv.(1) in + let quoted = Sys.argv.(1) = "-quoted" in + let ch_dir = Sys.argv.(if quoted then 2 else 1) in Sys.chdir ch_dir; let dir = Sys.getcwd () in - (* Needed for windows *) - let dir = Filename.quote dir in + let dir = if quoted then Filename.quote dir else dir in Format.printf "%s%!" dir diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 8a04206bb2..8732305953 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -23,7 +23,7 @@ Typeclasses Opaque id const flip compose arrow impl iff not all. (** Apply using the same opacity information as typeclass proof search. *) -Ltac class_apply c := autoapply c using typeclass_instances. +Ltac class_apply c := autoapply c with typeclass_instances. (** The unconvertible typeclass, to test that two objects of the same type are actually different. *) diff --git a/topbin/dune b/topbin/dune index f42e4d6fc2..e35a3de54b 100644 --- a/topbin/dune +++ b/topbin/dune @@ -36,3 +36,8 @@ (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin) (libraries coq.toplevel) (link_flags -linkall)) + +; Workers installed targets +(alias + (name topworkers) + (deps %{bin:coqqueryworker.opt} %{bin:coqtacticworker.opt} %{bin:coqproofworker.opt})) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index abfda07426..bbccae8edb 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -457,7 +457,7 @@ let parse_args ~help ~init arglist : t * string list = |"-batch" -> Flags.quiet := true; { oval with batch = true } - |"-test-mode" -> Flags.test_mode := true; oval + |"-test-mode" -> Vernacentries.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-boot" -> warn_deprecated_boot (); diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 11b64a5247..0d31992e98 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -16,7 +16,6 @@ open CAst open Util open Names open Nameops -open Term open Tacmach open Constrintern open Prettyp @@ -32,6 +31,7 @@ open Lemmas open Locality open Attributes +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (** TODO: make this function independent of Ltac *) @@ -133,22 +133,23 @@ let show_intro all = *) let make_cases_aux glob_ref = + let open Declarations in match glob_ref with | Globnames.IndRef ind -> - let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in + let mib, mip = Global.lookup_inductive ind in Util.Array.fold_right_i - (fun i typ l -> - let al = List.rev (fst (decompose_prod typ)) in - let al = Util.List.skipn np al in + (fun i (ctx, _) l -> + let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in let rec rename avoid = function | [] -> [] - | (n,_)::l -> + | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l + | RelDecl.LocalAssum (n, _)::l -> let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in Id.to_string n' :: rename (Id.Set.add n' avoid) l in let al' = rename Id.Set.empty al in let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) - tarr [] + mip.mind_nf_lc [] | _ -> raise Not_found let make_cases s = @@ -2377,6 +2378,8 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t +let test_mode = ref false + (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) let with_fail st b f = @@ -2402,7 +2405,7 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info + if not !Flags.quiet || !test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 4fbd3849b0..f43cec48e9 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -41,3 +41,7 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t + +(* Flag set when the test-suite is called. Its only effect to display + verbose information for `Fail` *) +val test_mode : bool ref |