diff options
64 files changed, 522 insertions, 367 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ec3702b360..3c427793e2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -10,7 +10,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-03-12-V1" + CACHEKEY: "bionic_coq-V2019-04-20-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/CHANGES.md b/CHANGES.md index ce8a787cd1..fc7272da65 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -227,6 +227,10 @@ Tools `coqc`/`make` as well as printing to stdout, on both python2 and python3. +- Coq options can be set on the command line, eg `-set "Universe Polymorphism=true"` + +- coq_makefile's install target now errors if any file to install is missing. + Standard Library - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about diff --git a/Makefile.ide b/Makefile.ide index 908f5f6648..8f9088a04a 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -66,7 +66,7 @@ IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_ GTKSHARE=$(shell pkg-config --variable=prefix gtk+-3.0)/share GTKBIN=$(shell pkg-config --variable=prefix gtk+-3.0)/bin GTKLIBS=$(shell pkg-config --variable=libdir gtk+-3.0) -PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-3.0)/bin +PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-3.0)/share ########################################################################### @@ -244,15 +244,15 @@ $(COQIDEAPP)/Contents: $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ - -linkpkg -package str,unix,dynlink,threads,lablgtk3.sourceview3 $(IDEFLAGS:.cma=.cmxa) $^ + -linkpkg -package str,unix,dynlink,threads,lablgtk3-sourceview3 $(IDEFLAGS:.cma=.cmxa) $^ $(STRIP_HIDE) $@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents $(MKDIR) $@/coq/ $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $@/coq/ - $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} - $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ - $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ + $(MKDIR) $@/gtksourceview-3.0/{language-specs,styles} + $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-3.0/language-specs/ + $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/ cp -R "$(GTKSHARE)/"locale $@ cp -R "$(GTKSHARE)/"themes $@ @@ -262,20 +262,20 @@ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-3.0/3.0.0/immodules/"*.so $@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib $(MKDIR) $@/xdg/coq $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys - $(MKDIR) $@/gtk-2.0 + $(MKDIR) $@/gtk-3.0 { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-2.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ + > $@/gtk-3.0/gdk-pixbuf.loaders + { "$(GTKBIN)/gtk-query-immodules-3.0" $@/../immodules/*.so |\ sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-2.0/gtk-immodules.loaders + > $@/gtk-3.0/gtk-immodules.loaders $(MKDIR) $@/pango echo "[Pango]" > $@/pango/pangorc diff --git a/azure-pipelines.yml b/azure-pipelines.yml index a8b42cc722..6fcc64f77e 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -42,6 +42,9 @@ jobs: pool: vmImage: 'macOS-10.13' + variables: + MACOSX_DEPLOYMENT_TARGET: '10.12' + steps: - checkout: self fetchDepth: 10 @@ -49,16 +52,20 @@ jobs: - script: | set -e brew update - brew unlink python - brew install gnu-time opam + brew install gnu-time opam pkg-config gtksourceview3 + pip3 install macpack + displayName: 'Install system dependencies' + - script: | + set -e + export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig opam init -a -j "$NJOBS" --compiler=$COMPILER opam switch set $COMPILER eval $(opam env) opam update - opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit + opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 opam list - displayName: 'Install dependencies' + displayName: 'Install OCaml dependencies' env: COMPILER: "4.07.1" FINDLIB_VER: ".1.8.0" @@ -68,11 +75,30 @@ jobs: set -e eval $(opam env) - ./configure -local -warn-error yes -native-compiler no + ./configure -prefix '$(Build.BinariesDirectory)' -warn-error yes -native-compiler no -coqide opt make -j "$NJOBS" displayName: 'Build Coq' - script: | eval $(opam env) - make -j "$NJOBS" test-suite + make -j "$NJOBS" test-suite PRINT_LOGS=1 displayName: 'Run Coq Test Suite' + + - script: | + make install + displayName: 'Install Coq' + + - script: | + set -e + eval $(opam env) + export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig + ./dev/build/osx/make-macos-dmg.sh + mv _build/*.dmg "$(Build.ArtifactStagingDirectory)/" + displayName: 'Create the dmg bundle' + env: + OUTDIR: '$(Build.BinariesDirectory)' + + - task: PublishBuildArtifacts@1 + inputs: + pathtoPublish: '$(Build.ArtifactStagingDirectory)' + artifactName: coq-macOS-installer diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index c450e8157a..3a096fec06 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -4,7 +4,6 @@ set -e # Configuration setup -OUTDIR=$PWD/_install DMGDIR=$PWD/_dmg VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) APP=bin/CoqIDE_${VERSION}.app @@ -13,7 +12,7 @@ APP=bin/CoqIDE_${VERSION}.app make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP" # Add Coq to the .app file -make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop +make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources" install-coq install-ide-toploop # Create the dmg bundle mkdir -p "$DMGDIR" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index e553cbed1b..8eebb3af64 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-03-12-V1" +# CACHEKEY: "bionic_coq-V2019-04-20-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.05.0" # `num` does not have a version number as the right version to install varies # with the compiler version. ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \ - CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8" + CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh new file mode 100644 index 0000000000..1e1d36d54a --- /dev/null +++ b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then + + elpi_CI_REF=recarg-cleanup + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + quickchick_CI_REF=recarg-cleanup + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh new file mode 100644 index 0000000000..9a6e25d893 --- /dev/null +++ b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then + + elpi_CI_REF=overlay-elpi1.2-coq-master + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 416253fad1..40c3c32e4f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -83,6 +83,11 @@ Libobject * `Libobject.superglobal_object` * `Libobject.superglobal_object_nodischarge` +AST + +- Minor changes in the AST have been performed, for example + https://github.com/coq/coq/pull/9165 + Implicit Arguments - `Impargs.declare_manual_implicits` is restricted to only support declaration diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 56f84d0ff0..b410833d25 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -194,14 +194,14 @@ Program Fixpoint The optional order annotation follows the grammar: .. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + order : measure `term` [ `term` ] | wf `term` `ident` - + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on - any subset of the arguments and the optional (parenthesised) term - ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` - to ``lt``. + + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional term + :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R` + to :g:`lt`. - + :g:`wf R x` which is equivalent to :g:`measure x (R)`. + + :g:`wf R x` which is equivalent to :g:`measure x R`. The structural fixpoint operator behaves just like the one of |Coq| (see :cmd:`Fixpoint`), except it may also generate obligations. It works diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index eebf1f11e1..bdda35fcc0 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -210,6 +210,13 @@ and ``coqtop``, unless stated otherwise: is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. +:-set *string*: Enable flags and set options. *string* should be + ``Option Name=value``, the value is interpreted according to the + type of the option. For flags ``Option Name`` is equivalent to + ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` + will enable :flag:`Universe Polymorphism`. Note that the quotes are + shell syntax, Coq does not see them. +:-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. :-dump-glob *file*: Dump references for global names in file *file* diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index eaf1b2c2ad..0ade9fdbf5 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -149,13 +149,6 @@ class CoqObject(ObjectDescription): msg = MSG.format(name, self.env.doc2path(objects[name][0])) self.state_machine.reporter.warning(msg, line=self.lineno) - def _warn_if_duplicate_name(self, objects, name): - """Check that two objects in the same domain don't have the same name.""" - if name in objects: - MSG = 'Duplicate object: {}; other is at {}' - msg = MSG.format(name, self.env.doc2path(objects[name][0])) - self.state_machine.reporter.warning(msg, line=self.lineno) - def _record_name(self, name, target_id): """Record a name, mapping it to target_id diff --git a/ide/idetop.ml b/ide/idetop.ml index 10b8a2cdc5..543ff924bd 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -57,9 +57,9 @@ let coqide_known_option table = List.mem table [ ["Diffs"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (_, o, BoolValue true) - | VernacSetOption (_, o, StringValue _) - | VernacUnsetOption (_, o) -> coqide_known_option o + | VernacSetOption (_, o, OptionSetTrue) + | VernacSetOption (_, o, OptionSetString _) + | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) @@ -366,12 +366,13 @@ let get_options () = Goptions.OptionMap.fold fold table [] let set_options options = + let open Goptions in let iter (name, value) = match import_option_value value with - | BoolValue b -> Goptions.set_bool_option_value name b - | IntValue i -> Goptions.set_int_option_value name i - | StringValue s -> Goptions.set_string_option_value name s - | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen name + | BoolValue b -> set_bool_option_value name b + | IntValue i -> set_int_option_value name i + | StringValue s -> set_string_option_value name s + | StringOptValue (Some s) -> set_string_option_value name s + | StringOptValue None -> unset_option_value_gen name in List.iter iter options diff --git a/ide/macos_prehook.ml b/ide/macos_prehook.ml index d668788954..dc8fd0e85d 100644 --- a/ide/macos_prehook.ml +++ b/ide/macos_prehook.ml @@ -24,13 +24,13 @@ let () = Unix.putenv "GTK_DATA_PREFIX" resources_dir let () = Unix.putenv "GTK_EXE_PREFIX" resources_dir let () = Unix.putenv "GTK_PATH" resources_dir let () = - Unix.putenv "GTK2_RC_FILES" (Filename.concat etc_dir "gtk-2.0/gtkrc") + Unix.putenv "GTK3_RC_FILES" (Filename.concat etc_dir "gtk-3.0/gtkrc") let () = Unix.putenv "GTK_IM_MODULE_FILE" - (Filename.concat etc_dir "gtk-2.0/gtk-immodules.loaders") + (Filename.concat etc_dir "gtk-3.0/gtk-immodules.loaders") let () = Unix.putenv "GDK_PIXBUF_MODULE_FILE" - (Filename.concat etc_dir "gtk-2.0/gdk-pixbuf.loaders") + (Filename.concat etc_dir "gtk-3.0/gdk-pixbuf.loaders") let () = Unix.putenv "PANGO_LIBDIR" lib_dir let () = Unix.putenv "PANGO_SYSCONFIGDIR" etc_dir let () = Unix.putenv "CHARSETALIASDIR" lib_dir diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 7a14a4e708..9f778d99e9 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -134,16 +134,17 @@ and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - lident * (lident option * recursion_order_expr) * + lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr and cofix_expr = lident * local_binder_expr list * constr_expr * constr_expr -and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) +and recursion_order_expr_r = + | CStructRec of lident + | CWfRec of lident * constr_expr + | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *) +and recursion_order_expr = recursion_order_expr_r CAst.t (* Anonymous defs allowed ?? *) and local_binder_expr = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 60610b92b8..443473d5b6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -196,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 -and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = +and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = (eq_ast Id.equal id1 id2) && - Option.equal (eq_ast Id.equal) j1 j2 && - recursion_order_expr_eq r1 r2 && + Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -210,13 +209,17 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq a1 a2 && constr_expr_eq b1 b2 -and recursion_order_expr_eq r1 r2 = match r1, r2 with - | CStructRec, CStructRec -> true - | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 - | CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> +and recursion_order_expr_eq_r r1 r2 = match r1, r2 with + | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CWfRec (i1,e1), CWfRec (i2,e2) -> + constr_expr_eq e1 e2 + | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> + Option.equal (eq_ast Id.equal) i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false +and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 + and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 @@ -349,7 +352,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> + List.fold_right (fun (_,ro,lb,t,c) acc -> fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b89b6b5765..488c9a740f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -738,6 +738,14 @@ let extern_optimal extern r r' = | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match +(* Helper function for safe and optimal printing of primitive tokens *) +(* such as those for Int63 *) +let extern_prim_token_delimiter_if_required n key_n scope_n scopes = + match availability_of_prim_token n scope_n scopes with + | Some None -> CPrim n + | None -> CDelimiters(key_n, CAst.make (CPrim n)) + | Some (Some key) -> CDelimiters(key, CAst.make (CPrim n)) + (**********************************************************************) (* mapping decl *) @@ -938,13 +946,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r = let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in - let n = - match fst nv.(i) with - | None -> None - | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) - in - let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, + let n = + match nv.(i) with + | None -> None + | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x))) + in + ((CAst.make fi), n, bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) @@ -967,8 +974,11 @@ let rec extern inctx (custom,scopes as allscopes) vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, map_cast_type (extern_typ scopes vars) c') + | GInt i -> - CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i))) + extern_prim_token_delimiter_if_required + (Numeral (SPlus, NumTok.int (Uint63.to_string i))) + "int63" "int63_scope" (snd scopes) in insert_coercion coercion (CAst.make ?loc c) @@ -1159,13 +1169,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function let lonely_seen = add_lonely keyrule lonely_seen in extern_notation allscopes lonely_seen vars t rules -and extern_recursion_order scopes vars = function - GStructRec -> CStructRec - | GWfRec c -> CWfRec (extern true scopes vars c) - | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, - Option.map (extern true scopes vars) r) - - let extern_glob_constr vars c = extern false (InConstrEntrySomeLevel,(None,[])) vars c @@ -1294,7 +1297,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with let v = Array.map3 (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) bl tl ln in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3329ba2047..c0801067ce 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1845,51 +1845,44 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in - let n = - try List.index0 Id.equal iddef lf + let n = + try List.index0 Id.equal iddef lf with Not_found -> - raise (InternalizationError (locid,UnboundFixName (false,iddef))) - in - let idl_temp = Array.map - (fun (id,(n,order),bl,ty,_) -> - let intern_ro_arg f = - let before, after = split_at_annot bl n in - let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in - let ro = f (intern env') in - let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with - | GLocalAssum _ -> true - | _ -> false (* remove let-ins *)) - rbefore) n in - n', ro, List.fold_left intern_local_binder (env',rbefore) after - in - let n, ro, (env',rbl) = - match order with - | CStructRec -> - intern_ro_arg (fun _ -> GStructRec) - | CWfRec c -> - intern_ro_arg (fun f -> GWfRec (f c)) - | CMeasureRec (m,r) -> - intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) - in - let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - ((n, ro), bl, intern_type env' ty, env')) dl in + raise (InternalizationError (locid,UnboundFixName (false,iddef))) + in + let idl_temp = Array.map + (fun (id,recarg,bl,ty,_) -> + let recarg = Option.map (function { CAst.v = v } -> match v with + | CStructRec i -> i + | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg + in + let before, after = split_at_annot bl recarg in + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in + let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with + | GLocalAssum _ -> true + | _ -> false (* remove let-ins *)) + rbefore) recarg in + let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + (n, bl, intern_type env' ty, env')) dl in let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in - push_name_env ntnvars (impls_type_list ~args:fix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in - DAst.make ?loc @@ - GRec (GFix - (Array.map (fun (ro,_,_,_) -> ro) idl,n), + let env'' = List.fold_left_i (fun i en name -> + let (_,bli,tyi,_) = idl_temp.(i) in + let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) + en (CAst.make @@ Name name)) 0 env' lf in + (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + DAst.make ?loc @@ + GRec (GFix + (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) + | CCoFix ({ CAst.loc = locid; v = iddef }, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in let dl = Array.of_list dl in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 9801e56ca1..7f084fffdd 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -957,7 +957,7 @@ let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 | GFix (nl1,n1), GFix (nl2,n2) -> - let test (n1, _) (n2, _) = match n1, n2 with + let test n1 n2 = match n1, n2 with | _, None -> true | Some id1, Some id2 -> Int.equal id1 id2 | _ -> false diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 6fe20486dc..5024f5c26f 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -38,7 +38,7 @@ type notation_constr = notation_constr * notation_constr | NIf of notation_constr * (Name.t * notation_constr option) * notation_constr * notation_constr - | NRec of fix_kind * Id.t array * + | NRec of glob_fix_kind * Id.t array * (Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array | NSort of glob_sort diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index baa290367f..d153f84e9c 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open CErrors open Names open Nativelib open Reduction @@ -152,19 +151,15 @@ let native_conv_gen pb sigma env univs t1 t2 = else let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in - match compile ml_filename code ~profile:false with - | (true, fn) -> - begin - if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); - let t0 = Sys.time () in - call_linker ~fatal:true prefix fn (Some upds); - let t1 = Sys.time () in - let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); - (* TODO change 0 when we can have de Bruijn *) - fst (conv_val env pb 0 !rt1 !rt2 univs) - end - | _ -> anomaly (Pp.str "Compilation failure.") + let fn = compile ml_filename code ~profile:false in + if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); + let t0 = Sys.time () in + call_linker ~fatal:true prefix fn (Some upds); + let t1 = Sys.time () in + let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in + if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + (* TODO change 0 when we can have de Bruijn *) + fst (conv_val env pb 0 !rt1 !rt2 univs) (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 833e4082f0..43c9676f05 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -56,14 +56,15 @@ let write_ml_code fn ?(header=[]) code = List.iter (pp_global fmt) (header@code); close_out ch_out -let warn_native_compiler_failed = - let print = function +let error_native_compiler_failed e = + let msg = match e with + | Inl (Unix.WEXITED 127) -> Pp.(strbrk "The OCaml compiler was not found. Make sure it is installed, together with findlib.") | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n) | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n) | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n) | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e)) in - CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print + CErrors.user_err msg let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in @@ -100,15 +101,12 @@ let call_compiler ?profile:(profile=false) ml_filename = if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (Envars.ocamlfind ()) args in - let res = match res with - | Unix.WEXITED 0 -> true - | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n -> - warn_native_compiler_failed (Inl res); false - in - res, link_filename + match res with + | Unix.WEXITED 0 -> link_filename + | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n -> + error_native_compiler_failed (Inl res) with Unix.Unix_error (e,_,_) -> - warn_native_compiler_failed (Inr e); - false, link_filename + error_native_compiler_failed (Inr e) let compile fn code ~profile:profile = write_ml_code fn code; @@ -128,9 +126,8 @@ let compile_library dir code fn = in let fn = dirname / basename in write_ml_code fn ~header code; - let r = fst (call_compiler fn) in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; - r + let _ = call_compiler fn in + if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn (* call_linker links dynamically the code for constants in environment or a *) (* conversion test. *) diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 25adcf224b..e113350368 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -21,9 +21,14 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> profile:bool -> bool * string - -val compile_library : Names.DirPath.t -> global list -> string -> bool +(** [compile file code ~profile] will compile native [code] to [file], + and return the name of the object file; this name depends on + whether are in byte mode or not; file is expected to be .ml file *) +val compile : string -> global list -> profile:bool -> string + +(** [compile_library lib code file] is similar to [compile file code] + but will perform some extra tweaks to handle [code] as a Coq lib. *) +val compile_library : Names.DirPath.t -> global list -> string -> unit val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit diff --git a/library/goptions.mli b/library/goptions.mli index 9925eb9e7b..2e593e9d9e 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -172,6 +172,14 @@ type option_value = | StringValue of string | StringOptValue of string option +val set_option_value : ?locality:option_locality -> + ('a -> option_value -> option_value) -> option_name -> 'a -> unit +(** [set_option_value ?locality f name v] sets [name] to the result of + applying [f] to [v] and [name]'s current value. Use for behaviour + depending on the type of the option, eg erroring when ['a] doesn't + match it. Changing the type will result in errors later so don't do + that. *) + (** Summary of an option status *) type option_state = { opt_depr : bool; diff --git a/library/library.ml b/library/library.ml index 37dadadb76..04e38296d9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -718,8 +718,7 @@ let save_library_to ?todo ~output_native_objects dir f otab = (* Writing native code files *) if output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - if not (Nativelib.compile_library dir ast fn) then - user_err Pp.(str "Could not compile the library to native code.") + Nativelib.compile_library dir ast fn with reraise -> let reraise = CErrors.push reraise in let () = Feedback.msg_warning (str "Removed file " ++ str f') in diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 0586dda555..4a9190c10a 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = - let _ = Option.map (fun { CAst.loc = aloc } -> + Option.iter (fun { CAst.loc = aloc } -> CErrors.user_err ?loc:aloc ~hdr:"Constr:mk_cofixb" - (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in + (Pp.str"Annotation forbidden in cofix expression.")) ann; let ty = match tyc with Some ty -> ty | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in @@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) } - | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) } + [ [ "{"; IDENT "struct"; id=identref; "}" -> { CAst.make ~loc @@ CStructRec id } + | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CAst.make ~loc @@ CWfRec(id,rel) } | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) } + rel=OPT constr; "}" -> { CAst.make ~loc @@ CMeasureRec (id,m,rel) } ] ] ; impl_name_head: @@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> { (assum na :: fst bl), snd bl } - | f = fixannot -> { [], f } + | f = fixannot -> { [], Some f } | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } - | -> { [], (None, CStructRec) } + | -> { [], None } ] ] ; open_binders: diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5d8897cb47..3a57c14a3b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -191,7 +191,7 @@ module Constr : val binder : local_binder_expr list Entry.t (* closed_binder or variable *) val binders : local_binder_expr list Entry.t (* list of binder *) val open_binders : local_binder_expr list Entry.t - val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t + val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 4e8cf80ed2..a3973732ad 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -179,8 +179,10 @@ let () = VERNAC COMMAND EXTEND Function | ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] => { let hard = List.exists (function - | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true - | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in + | _,((_,(Some { CAst.v = CMeasureRec _ } + | Some { CAst.v = CWfRec _}),_,_,_),_) -> true + | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) + | _,((_,None,_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e582362e25..6494e90a03 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -469,11 +469,6 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas CAst.(with_val (fun x -> x)) (Constrexpr_ops.names_of_local_assums args) in - match wf_arg with - | None -> - if Int.equal (List.length names) 1 then 1 - else error "Recursive argument must be specified" - | Some wf_arg -> List.index Name.equal (Name wf_arg) names in let unbounded_eq = @@ -575,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas in wf_rel_with_mes,false in - register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes (Some wf_arg) + register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg using_lemmas args ret_type body let map_option f = function @@ -623,15 +618,15 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = - List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> + List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in - (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixpoint_exprl constr_expr_typel in @@ -643,7 +638,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let pstate, _is_struct = match fixpoint_exprl with - | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> + | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e @@ -665,9 +660,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive true in if register_built - then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false + then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false else pstate, false - |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> + |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e @@ -692,9 +687,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true else pstate, true | _ -> - List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> + List.iter (function ((_na,ord,_args,_body,_type),_not) -> match ord with - | Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _ -> + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> error ("Cannot use mutual definition with well-founded recursion or measure") | _ -> () @@ -869,38 +864,42 @@ let make_graph ~pstate (f_ref : GlobRef.t) = ) () in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b.CAst.v with - | Constrexpr.CFix(l_id,fixexprl) -> - let l = - List.map - (fun (id,(n,recexp),bl,t,b) -> - let { CAst.loc; v=rec_id } = Option.get n in - let new_args = - List.flatten - (List.map - (function - | Constrexpr.CLocalDef (na,_,_)-> [] - | Constrexpr.CLocalAssum (nal,_,_) -> - List.map - (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) - nal - | Constrexpr.CLocalPattern _ -> assert false - ) - nal_tas - ) - in - let b' = add_args id.CAst.v new_args b in - ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixexprl - in - l + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> + let l = + List.map + (fun (id,recexp,bl,t,b) -> + let { CAst.loc; v=rec_id } = match Option.get recexp with + | { CAst.v = CStructRec id } -> id + | { CAst.v = CWfRec (id,_) } -> id + | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid + in + let new_args = + List.flatten + (List.map + (function + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> + List.map + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) + nal + | Constrexpr.CLocalPattern _ -> assert false + ) + nal_tas + ) + in + let b' = add_args id.CAst.v new_args b in + ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ) + fixexprl + in + l | _ -> let id = Label.to_id (Constant.label c) in - [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [((CAst.make id,None),None,nal_tas,t,Some b),[]] in let mp = Constant.modpath c in let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7cd62f4ead..f44962f213 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1200,7 +1200,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, - { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> + { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } -> let bs = format_local_binders h bl in let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c @@ -1424,7 +1424,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd } | [] -> CErrors.user_err (Pp.str "Bad structural argument") in loop (names_of_local_assums lb) in let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in - let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in + let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some (CAst.make (CStructRec i))), lb, t', c']) in id, ((fk, h'), { ac with body = fix }) } END diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0a0d9b12fa..bf7f082192 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -183,7 +183,7 @@ GRAMMAR EXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) } + { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) } ] ] ; END diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index eaa5736336..062e3ca8b2 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -653,7 +653,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let v = Array.map3 (fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 6da168711c..85b9faac77 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -106,19 +106,9 @@ let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && Option.equal f c1 c2 && f t1 t2 -let fix_recursion_order_eq f o1 o2 = match o1, o2 with - | GStructRec, GStructRec -> true - | GWfRec c1, GWfRec c2 -> f c1 c2 - | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - f c1 c2 && Option.equal f o1 o2 - | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false - -let fix_kind_eq f k1 k2 = match k1, k2 with +let fix_kind_eq k1 k2 = match k1, k2 with | GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a2 + Int.equal i1 i2 && Array.equal (Option.equal Int.equal) a1 a2 | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 | (GFix _ | GCoFix _), _ -> false @@ -150,7 +140,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> - fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 | GSort s1, GSort s2 -> glob_sort_eq s1 s2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index c57cf88cc6..02cb294f6d 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -41,6 +41,12 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level type sort_info = (Libnames.qualid * int) option list type glob_sort = sort_info glob_sort_gen +type glob_recarg = int option + +and glob_fix_kind = + | GFix of (glob_recarg array * int) + | GCoFix of int + (** Casts *) type 'a cast_type = @@ -78,7 +84,7 @@ type 'a glob_constr_r = (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * + | GRec of glob_fix_kind * Id.t array * 'a glob_decl_g list array * 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option @@ -88,15 +94,6 @@ and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g -and 'a fix_recursion_order_g = - | GStructRec - | GWfRec of 'a glob_constr_g - | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - -and 'a fix_kind_g = - | GFix of ((int option * 'a fix_recursion_order_g) array * int) - | GCoFix of int - and 'a predicate_pattern_g = Name.t * (inductive * Name.t list) CAst.t option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) @@ -117,9 +114,7 @@ type tomatch_tuples = [ `any ] tomatch_tuples_g type cases_clause = [ `any ] cases_clause_g type cases_clauses = [ `any ] cases_clauses_g type glob_decl = [ `any ] glob_decl_g -type fix_kind = [ `any ] fix_kind_g type predicate_pattern = [ `any ] predicate_pattern_g -type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0003fc7280..e694502231 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -492,25 +492,23 @@ let native_norm env sigma c ty = Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); *) - 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 - match Nativelib.compile ml_filename code ~profile:profile with - | true, fn -> - if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); - let profiler_pid = if profile then start_profiler () else None in - let t0 = Sys.time () in - Nativelib.call_linker ~fatal:true 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 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); - EConstr.of_constr res - | _ -> anomaly (Pp.str "Compilation failure.") + 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 fn = Nativelib.compile ml_filename code ~profile:profile in + if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); + let profiler_pid = if profile then start_profiler () else None in + let t0 = Sys.time () in + Nativelib.call_linker ~fatal:true 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 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); + EConstr.of_constr res let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b29afd1fd2..c788efda48 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -470,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PCase (info, pred, pat_of_raw metas vars c, brs) | GRec (GFix (ln,n), ids, decls, tl, cl) -> - if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then - err ?loc (Pp.str "\"struct\" annotation is expected.") - else - let ln = Array.map (fst %> Option.get) ln in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in - let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in - let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in - let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in - let names = Array.map (fun id -> Name id) ids in - PFix ((ln,n), (names, tl, cl)) + let get_struct_arg = function + | Some n -> n + | None -> err ?loc (Pp.str "\"struct\" annotation is expected.") + (* TODO why can't the annotation be omitted? *) + in + let ln = Array.map get_struct_arg ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) | GRec (GCoFix n, ids, decls, tl, cl) -> let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0f7676cd19..48d981082c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env fixpoints ?) *) let possible_indexes = Array.to_list (Array.mapi - (fun i (n,_) -> match n with + (fun i annot -> match annot with | Some n -> [n] | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) - vn) + vn) in let fixdecls = (names,ftys,fdefs) in let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0ae3de7321..78733784a7 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -399,12 +399,12 @@ let tag_var = tag Tag.variable pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c - let pr_guard_annot pr_aux bl (n,ro) = - match n with + let pr_guard_annot pr_aux bl ro = + match ro with | None -> mt () - | Some {loc; v = id} -> - match (ro : Constrexpr.recursion_order_expr) with - | CStructRec -> + | Some {loc; v = ro} -> + match ro with + | CStructRec { v = id } -> let names_of_binder = function | CLocalAssum (nal,_,_) -> nal | CLocalDef (_,_,_) -> [] @@ -413,10 +413,11 @@ let tag_var = tag Tag.variable if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" else mt() - | CWfRec c -> - spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" - | CMeasureRec (m,r) -> - spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ + | CWfRec (id,c) -> + spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}" + | CMeasureRec (id,m,r) -> + spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ + match id with None -> mt() | Some id -> spc () ++ pr_lident id ++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index db1687a49b..1332cd0168 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -35,10 +35,11 @@ val pr_patvar : Pattern.patvar -> Pp.t val pr_glob_level : Glob_term.glob_level -> Pp.t val pr_glob_sort : Glob_term.glob_sort -> Pp.t -val pr_guard_annot : (constr_expr -> Pp.t) -> - local_binder_expr list -> - lident option * recursion_order_expr -> - Pp.t +val pr_guard_annot + : (constr_expr -> Pp.t) + -> local_binder_expr list + -> recursion_order_expr option + -> Pp.t val pr_record_body : (qualid * constr_expr) list -> Pp.t val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index d042a1d650..f378a5d2dd 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -438,18 +438,18 @@ let match_goals ot nt = | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)") in let recursion_order_expr ogname exp exp2 = - match exp, exp2 with - | CStructRec, CStructRec -> () - | CWfRec c, CWfRec c2 -> + match exp.CAst.v, exp2.CAst.v with + | CStructRec _, CStructRec _ -> () + | CWfRec (_,c), CWfRec (_,c2) -> constr_expr ogname c c2 - | CMeasureRec (m,r), CMeasureRec (m2,r2) -> + | CMeasureRec (_,m,r), CMeasureRec (_,m2,r2) -> constr_expr ogname m m2; constr_expr_opt ogname r r2 | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)") in let fix_expr ogname exp exp2 = - let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in - recursion_order_expr ogname ro ro2; + let (l,ro,lb,ce1,ce2), (l2,ro2,lb2,ce12,ce22) = exp,exp2 in + Option.iter2 (recursion_order_expr ogname) ro ro2; iter2 (local_binder_expr ogname) lb lb2; constr_expr ogname ce1 ce12; constr_expr ogname ce2 ce22 diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index d1bd3692ab..2493b1fac4 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -139,7 +139,7 @@ module Make(T : Task) () = struct (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file" - | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" + | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl (* We need to pass some options with two arguments *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 58fe923f9e..243b5c333d 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -57,6 +57,7 @@ let options_affecting_stm_scheduling = stm_allow_nested_proofs_option_name; Vernacentries.proof_mode_opt_name; Attributes.program_mode_option_name; + Proof_using.proof_using_opt_name; ] let classify_vernac e = @@ -64,7 +65,7 @@ let classify_vernac e = (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) - | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) + | VernacSetOption (_, l,_) when CList.exists (CList.equal String.equal l) options_affecting_stm_scheduling -> VtSideff [], VtNow @@ -91,9 +92,6 @@ let classify_vernac e = VtProofStep { parallel = `No; proof_block_detection = Some "curly" }, VtLater - (* Options changing parser *) - | VernacUnsetOption (_, ["Default";"Proof";"Using"]) - | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater @@ -156,7 +154,7 @@ let classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacSetOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index d1b77f3758..16829482e5 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -181,10 +181,7 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.concat_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) [ind, s]) - Safe_typing.empty_private_constants + s, Safe_typing.empty_private_constants let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind diff --git a/test-suite/coq-makefile/missing-install/run.sh b/test-suite/coq-makefile/missing-install/run.sh new file mode 100755 index 0000000000..4f36fdcb1c --- /dev/null +++ b/test-suite/coq-makefile/missing-install/run.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash + +. ../template/init.sh + +rm -rf _test; mkdir _test; cd _test + +cat > _CoqProject <<EOF +-R theories Test +theories/a.v +theories/b.v +EOF +mkdir theories +touch theories/a.v theories/b.v + +coq_makefile -f _CoqProject -o Makefile +make theories/b.vo +if make install; then exit 1; fi diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index fdd5599565..4d76f1210b 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -1,3 +1,7 @@ +2%int63 + : int +(2 + 2)%int63 + : int 2 : int 9223372036854775807 @@ -14,3 +18,15 @@ The command has indeed failed with message: int63 are only non-negative numbers. The command has indeed failed with message: overflow in int63 literal: 9223372036854775808 +2 + : nat +2%int63 + : int +t = 2%i63 + : int +t = 2%i63 + : int +2 + : nat +2 + : int diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 3dc364eddb..0385e529bf 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -1,5 +1,7 @@ Require Import Int63 Cyclic63. +Check 2%int63. +Check (2 + 2)%int63. Open Scope int63_scope. Check 2. Check 9223372036854775807. @@ -9,4 +11,15 @@ Eval vm_compute in 2+2. Eval vm_compute in 65675757 * 565675998. Fail Check -1. Fail Check 9223372036854775808. +Open Scope nat_scope. +Check 2. (* : nat *) +Check 2%int63. +Delimit Scope int63_scope with i63. +Definition t := 2%int63. +Print t. +Delimit Scope nat_scope with int63. +Print t. +Check 2. +Close Scope nat_scope. +Check 2. Close Scope int63_scope. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 85d7a770fc..02adb012d9 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -13,7 +13,7 @@ Print sigT_rect. Obligation Tactic := program_simplify ; auto with *. About MR. -Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat := +Program Fixpoint merge (n m : nat) {measure (n + m) lt} : nat := match n with | 0 => 0 | S n' => merge n' m @@ -101,5 +101,5 @@ Next Obligation. simpl in *; intros. Qed. Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) - {measure (p - n) p} : nat := + {measure (p - n)} : nat := _. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index bd9d8c9221..0236c549d5 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -468,6 +468,9 @@ beautify: $(BEAUTYFILES) # Extensions can't assume when they run. install: + $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code $(HIDE)for f in $(FILESTOINSTALL); do\ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ if [ "$$?" != "0" -o -z "$$df" ]; then\ diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index bf1297d661..319f5c8ad6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -38,6 +38,8 @@ type color = [`ON | `AUTO | `OFF] type native_compiler = NativeOff | NativeOn of { ondemand : bool } +type option_command = OptionSet of string option | OptionUnset + type t = { load_init : bool; @@ -63,6 +65,8 @@ type t = { allow_sprop : bool; cumulative_sprop : bool; + set_options : (Goptions.option_name * option_command) list; + stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; @@ -115,6 +119,8 @@ let default = { allow_sprop = false; cumulative_sprop = false; + set_options = []; + stm_flags = Stm.AsyncOpts.default_opts; debug = false; diffs_set = false; @@ -245,6 +251,16 @@ let get_native_name s = Nativelib.output_dir; Library.native_name_from_filename s] with _ -> "" +let to_opt_key = Str.(split (regexp " +")) + +let parse_option_set opt = + match String.index_opt opt '=' with + | None -> to_opt_key opt, None + | Some eqi -> + let len = String.length opt in + let v = String.sub opt (eqi+1) (len - eqi - 1) in + to_opt_key (String.sub opt 0 eqi), Some v + (*s Parsing of the command line. We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) @@ -450,6 +466,16 @@ let parse_args ~help ~init arglist : t * string list = in { oval with native_compiler } + | "-set" -> + let opt = next() in + let opt, v = parse_option_set opt in + { oval with set_options = (opt, OptionSet v) :: oval.set_options } + + | "-unset" -> + let opt = next() in + let opt = to_opt_key opt in + { oval with set_options = (opt, OptionUnset) :: oval.set_options } + (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 97a62e97e4..9bcfdca332 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -14,6 +14,8 @@ val default_toplevel : Names.DirPath.t type native_compiler = NativeOff | NativeOn of { ondemand : bool } +type option_command = OptionSet of string option | OptionUnset + type t = { load_init : bool; @@ -38,6 +40,8 @@ type t = { allow_sprop : bool; cumulative_sprop : bool; + set_options : (Goptions.option_name * option_command) list; + stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index b3de8dd85f..4129562065 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -340,9 +340,7 @@ let print_anyway_opts = [ let print_anyway c = let open Vernacexpr in match c with - | VernacExpr (_, VernacSetOption (_, opt, _)) - | VernacExpr (_, VernacUnsetOption (_, opt)) -> - List.mem opt print_anyway_opts + | VernacExpr (_, VernacSetOption (_, opt, _)) -> List.mem opt print_anyway_opts | _ -> false (* We try to behave better when goal printing raises an exception diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 626023737b..8fae561be8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -50,6 +50,41 @@ let print_memory_stat () = let _ = at_exit print_memory_stat +let interp_set_option opt v old = + let open Goptions in + let err expect = + let opt = String.concat " " opt in + let got = v in (* avoid colliding with Pp.v *) + CErrors.user_err + Pp.(str "-set: " ++ str opt ++ + str" expects " ++ str expect ++ + str" but got " ++ str got) + in + match old with + | BoolValue _ -> + let v = match String.trim v with + | "true" -> true + | "false" | "" -> false + | _ -> err "a boolean" + in + BoolValue v + | IntValue _ -> + let v = String.trim v in + let v = match int_of_string_opt v with + | Some _ as v -> v + | None -> if v = "" then None else err "an int" + in + IntValue v + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) + +let set_option = let open Goptions in function + | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt + | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v + +let set_options = List.iter set_option + (******************************************************************************) (* Input/Output State *) (******************************************************************************) @@ -195,6 +230,8 @@ let init_toplevel ~help ~init custom_init arglist = Global.set_allow_sprop opts.allow_sprop; if opts.cumulative_sprop then Global.make_sprop_cumulative (); + set_options opts.set_options; + (* Allow the user to load an arbitrary state here *) inputstate opts; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 513374c2af..7074215afe 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -74,6 +74,9 @@ let print_usage_common co command = \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ \n -mangle-names x mangle auto-generated names using prefix x\ +\n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ +\n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ +\n -unset \"Foo Bar\" disable Foo Bar (as Unset Foo Bar. in a file)\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 2aadbd224f..1912646ffd 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -329,16 +329,27 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; pstate -let extract_decreasing_argument limit = function - | (na,CStructRec) -> na - | (na,_) when not limit -> na +let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with + | CStructRec na -> na + | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na + | CMeasureRec (None,_,_) when not structonly -> + user_err Pp.(str "Decreasing argument must be specificed in measure clause.") | _ -> user_err Pp.(str - "Only structural decreasing is supported for a non-Program Fixpoint") + "Well-founded induction requires Program Fixpoint or Function.") -let extract_fixpoint_components limit l = +let extract_fixpoint_components ~structonly l = let fixl, ntnl = List.split l in let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) -> - let ann = extract_decreasing_argument limit ann in + (* This is a special case: if there's only one binder, we pick it as the + recursive argument if none is provided. *) + let ann = Option.map (fun ann -> match bl, ann with + | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | _, x -> x) ann + in + let ann = Option.map (extract_decreasing_argument ~structonly) ann in {fix_name = id; fix_annot = ann; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in fixl, List.flatten ntnl @@ -356,7 +367,7 @@ let check_safe () = flags.check_universes && flags.check_guarded let do_fixpoint ~ontop local poly l = - let fixl, ntns = extract_fixpoint_components true l in + let fixl, ntns = extract_fixpoint_components ~structonly:true l in let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 15ff5f4498..5937842f17 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -62,7 +62,7 @@ val interp_recursive : (** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : bool -> +val extract_fixpoint_components : structonly:bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 350b2d2945..20a2db7ca2 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -85,7 +85,7 @@ let rec telescope sigma l = let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx -let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = +let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let open EConstr in let open Vars in let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in @@ -304,22 +304,26 @@ let do_program_recursive local poly fixkind fixl ntns = let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with - | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> - let recarg = - match n with - | Some n -> mkIdentC n.CAst.v - | None -> - user_err ~hdr:"do_program_fixpoint" - (str "Recursive argument required for well-founded fixpoints") - in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn + | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + let recarg = mkIdentC n.CAst.v in + build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn - | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> - build_wellfounded (id, pl, n, bl, typ, out_def def) poly + | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *) + let r = match n, r with + | Some id, None -> + let loc = id.CAst.loc in + Some (CAst.make ?loc @@ CRef(qualid_of_ident ?loc id.CAst.v,None)) + | Some _, Some _ -> + user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") + | _, _ -> r + in + build_wellfounded (id, pl, bl, typ, out_def def) poly (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn - | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> - let fixl,ntns = extract_fixpoint_components true l in - let fixkind = Obligations.IsFixpoint g in + | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> + let fixl,ntns = extract_fixpoint_components ~structonly:true l in + let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in do_program_recursive local poly fixkind fixl ntns | _, _ -> diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1533d0ccd3..3f491d1dd4 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -875,10 +875,10 @@ GRAMMAR EXTEND Gram GLOBAL: command query_command class_rawexpr gallina_ext; gallina_ext: - [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> + [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting -> { VernacSetOption (true, table, v) } | IDENT "Export"; IDENT "Unset"; table = option_table -> - { VernacUnsetOption (true, table) } + { VernacSetOption (true, table, OptionUnset) } ] ]; command: @@ -943,10 +943,10 @@ GRAMMAR EXTEND Gram { VernacAddMLPath (true, dir) } (* For acting on parameter tables *) - | "Set"; table = option_table; v = option_value -> + | "Set"; table = option_table; v = option_setting -> { VernacSetOption (false, table, v) } | IDENT "Unset"; table = option_table -> - { VernacUnsetOption (false, table) } + { VernacSetOption (false, table, OptionUnset) } | IDENT "Print"; IDENT "Table"; table = option_table -> { VernacPrintOption table } @@ -1057,10 +1057,10 @@ GRAMMAR EXTEND Gram | IDENT "Library"; qid = global -> { LocateLibrary qid } | IDENT "Module"; qid = global -> { LocateModule qid } ] ] ; - option_value: - [ [ -> { BoolValue true } - | n = integer -> { IntValue (Some n) } - | s = STRING -> { StringValue s } ] ] + option_setting: + [ [ -> { OptionSetTrue } + | n = integer -> { OptionSetInt n } + | s = STRING -> { OptionSetString s } ] ] ; option_ref_value: [ [ id = global -> { QualidRefValue id } @@ -1130,10 +1130,10 @@ GRAMMAR EXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - { VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) } + { VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue) } | IDENT "Debug"; IDENT "Off" -> - { VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) } + { VernacSetOption (false, ["Ltac";"Debug"], OptionUnset) } (* registration of a custom reduction *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 07194578c1..1b1c618dc7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -295,7 +295,7 @@ type obligation = type obligations = (obligation array * int) type fixpoint_kind = - | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of lident option list | IsCoFixpoint type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list @@ -486,7 +486,7 @@ let rec lam_index n t acc = lam_index n b (succ acc) | _ -> raise Not_found -let compute_possible_guardness_evidences (n,_) fixbody fixtype = +let compute_possible_guardness_evidences n fixbody fixtype = match n with | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] | None -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index b1b7b1ec90..d25daeed9c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -70,7 +70,7 @@ type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list + | IsFixpoint of lident option list | IsCoFixpoint val add_mutual_definitions : diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b602e134da..4e4d431e89 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -173,15 +173,10 @@ open Pputils pr_opt (prlist_with_sep sep pr_option_ref_value) b let pr_set_option a b = - let pr_opt_value = function - | IntValue None -> assert false - (* This should not happen because of the grammar *) - | IntValue (Some n) -> spc() ++ int n - | StringValue s -> spc() ++ str s - | StringOptValue None -> mt() - | StringOptValue (Some s) -> spc() ++ str s - | BoolValue b -> mt() - in pr_printoption a None ++ pr_opt_value b + pr_printoption a None ++ (match b with + | OptionUnset | OptionSetTrue -> mt() + | OptionSetInt n -> spc() ++ int n + | OptionSetString s -> spc() ++ quote (str s)) let pr_opt_hintbases l = match l with | [] -> mt() @@ -1140,15 +1135,11 @@ open Pputils hov 1 (keyword "Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) ) - | VernacUnsetOption (export, na) -> - let export = if export then keyword "Export" ++ spc () else mt () in - return ( - hov 1 (export ++ keyword "Unset" ++ spc() ++ pr_printoption na None) - ) | VernacSetOption (export, na,v) -> let export = if export then keyword "Export" ++ spc () else mt () in + let set = if v == OptionUnset then "Unset" else "Set" in return ( - hov 2 (export ++ keyword "Set" ++ spc() ++ pr_set_option na v) + hov 2 (export ++ keyword set ++ spc() ++ pr_set_option na v) ) | VernacAddOption (na,l) -> return ( diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 526845084a..1d089d0a55 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -172,11 +172,12 @@ let value = ref None let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us) let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us)) +let proof_using_opt_name = ["Default";"Proof";"Using"] let () = Goptions.(declare_stringopt_option { optdepr = false; optname = "default value for Proof using"; - optkey = ["Default";"Proof";"Using"]; + optkey = proof_using_opt_name; optread = (fun () -> Option.map using_to_string !value); optwrite = (fun b -> value := Option.map using_from_string b); }) diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 7d1110aaa2..702043a4a9 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -21,3 +21,6 @@ val suggest_constant : Environ.env -> Names.Constant.t -> unit val suggest_variable : Environ.env -> Names.Id.t -> unit val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option + +val proof_using_opt_name : string list +(** For the stm *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c24b9ec75..3a305c3b61 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1707,18 +1707,17 @@ let get_option_locality export local = let vernac_set_option0 ~local export key opt = let locality = get_option_locality export local in match opt with - | StringValue s -> set_string_option_value_gen ~locality key s - | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s - | StringOptValue None -> unset_option_value_gen ~locality key - | IntValue n -> set_int_option_value_gen ~locality key n - | BoolValue b -> set_bool_option_value_gen ~locality key b + | OptionUnset -> unset_option_value_gen ~locality key + | OptionSetString s -> set_string_option_value_gen ~locality key s + | OptionSetInt n -> set_int_option_value_gen ~locality key (Some n) + | OptionSetTrue -> set_bool_option_value_gen ~locality key true let vernac_set_append_option ~local export key s = let locality = get_option_locality export local in set_string_option_append_value_gen ~locality key s let vernac_set_option ~local export table v = match v with -| StringValue s -> +| OptionSetString s -> (* We make a special case for warnings because appending is their natural semantics *) if CString.List.equal table ["Warnings"] then @@ -1731,10 +1730,6 @@ let vernac_set_option ~local export table v = match v with vernac_set_option0 ~local export table v | _ -> vernac_set_option0 ~local export table v -let vernac_unset_option ~local export key = - let locality = get_option_locality export local in - unset_option_value_gen ~locality key - let vernac_add_option key lv = let f = function | StringRefValue s -> (get_string_table key)#add s @@ -2462,9 +2457,6 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = | VernacSetOption (export, key,v) -> vernac_set_option ~local:(only_locality atts) export key v; pstate - | VernacUnsetOption (export, key) -> - vernac_unset_option ~local:(only_locality atts) export key; - pstate | VernacRemoveOption (key,v) -> unsupported_attributes atts; vernac_remove_option key v; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ebfc473522..d0dae1aa53 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -109,11 +109,11 @@ type onlyparsing_flag = Flags.compat_version option which this notation is trying to be compatible with *) type locality_flag = bool (* true = Local *) -type option_value = Goptions.option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | StringOptValue of string option +type option_setting = + | OptionUnset + | OptionSetTrue + | OptionSetInt of int + | OptionSetString of string type option_ref_value = | StringRefValue of string @@ -129,7 +129,7 @@ type definition_expr = * constr_expr option type fixpoint_expr = - ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = ident_decl * local_binder_expr list * constr_expr * constr_expr option @@ -363,8 +363,7 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list - | VernacUnsetOption of export_flag * Goptions.option_name - | VernacSetOption of export_flag * Goptions.option_name * option_value + | VernacSetOption of export_flag * Goptions.option_name * option_setting | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list |