diff options
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | Makefile.install | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh | 9 | ||||
| -rw-r--r-- | doc/changelog/01-kernel/10811-sprop-default-on.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10888.v | 11 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 34 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 6 |
12 files changed, 63 insertions, 34 deletions
@@ -101,15 +101,18 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated -GENMLGFILES:= $(MLGFILES:.mlg=.ml) # GRAMFILES must be in linking order 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 +GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) +GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) +GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? + +GENMLGFILES:= $(MLGFILES:.mlg=.ml) +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml +GENMLIFILES:=$(GRAMMLIFILES) GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe -COQ_EXPORTED += GRAMFILES GRAMMLFILES GENGRAMFILES GENMLFILES GENHFILES GENFILES +COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES ## More complex file lists diff --git a/Makefile.build b/Makefile.build index f2e1ca4ea0..35f5e26272 100644 --- a/Makefile.build +++ b/Makefile.build @@ -203,7 +203,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) -allow-sprop +COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) # Beware this depends on the makefile being in a particular dir, we # should pass an absolute path here but windows is tricky # c.f. https://github.com/coq/coq/pull/9560 @@ -807,9 +807,9 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack MAINMLFILES := $(filter-out gramlib/.pack/% checker/% plugins/% user-contrib/%, $(MLFILES) $(MLIFILES)) MAINMLLIBFILES := $(filter-out gramlib/.pack/% checker/% plugins/% user-contrib/%, $(MLLIBFILES) $(MLPACKFILES)) -$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) $(GENGRAMFILES) +$(MLDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLFILES) $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP MLFILES MLIFILES' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) -passrest $(MAINMLFILES) -open Gramlib $(GRAMMLFILES) $(TOTARGET) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) -passrest $(MAINMLFILES) -open Gramlib $(GRAMMLFILES) $(GRAMMLIFILES) $(TOTARGET) #NB: -passrest is needed to avoid ocamlfind reordering the -open Gramlib $(MLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(MAINMLLIBFILES) $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) diff --git a/Makefile.install b/Makefile.install index 608e8a3c8e..456c391fd9 100644 --- a/Makefile.install +++ b/Makefile.install @@ -92,13 +92,13 @@ install-tools: INSTALLCMI = $(sort \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ - $(filter %.cmi, $(GRAMMLFILES:.mli=.cmi)) gramlib/.pack/gramlib.cmi \ + $(GRAMMLIFILES:.mli=.cmi) gramlib/.pack/gramlib.cmi \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ $(PLUGINS:.cmo=.cmi) INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \ configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \ - $(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx))) + $(GRAMMLFILES:.ml=.cmx) $(MLFILES:.ml=.cmx))) install-devfiles: $(MKDIR) $(FULLBINDIR) diff --git a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh new file mode 100644 index 0000000000..d7af6b7a36 --- /dev/null +++ b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then + + elpi_CI_REF=sprop-default-on + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + coq_dpdgraph_CI_REF=sprop-default-on + coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph + +fi diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst new file mode 100644 index 0000000000..349c44c205 --- /dev/null +++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst @@ -0,0 +1,3 @@ +- Using ``SProp`` is now allowed by default, without needing to pass + ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 + <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 8935ba27e3..9a9ec78edc 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -9,15 +9,16 @@ SProp (proof irrelevant propositions) This section describes the extension of |Coq| with definitionally proof irrelevant propositions (types in the sort :math:`\SProp`, also -known as strict propositions). To use :math:`\SProp` you must pass -``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`. +known as strict propositions). Using :math:`\SProp` may be prevented +by passing ``-disallow-sprop`` to the |Coq| program or using +:flag:`Allow StrictProp`. .. flag:: Allow StrictProp :name: Allow StrictProp Allows using :math:`\SProp` when set and forbids it when unset. The initial value depends on whether you used the command line - ``-allow-sprop``. + ``-disallow-sprop`` and ``-allow-sprop``. .. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag. :undocumented: diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v new file mode 100644 index 0000000000..3c2e8011d7 --- /dev/null +++ b/test-suite/bugs/closed/bug_10888.v @@ -0,0 +1,11 @@ + +Module Type T. +Context {A:Type}. +End T. + +Module M(X:T). + Import X. + Check X.A. + Check A. + Definition B := A. +End M. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d13ea707bb..d48d8b900f 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -38,10 +38,10 @@ Argument scopes are [type_scope _] bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) -foo@{u UnivBinders.17 v} = -Type@{UnivBinders.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,UnivBinders.17+1,v+1)} -(* u UnivBinders.17 v |= *) +foo@{u UnivBinders.18 v} = +Type@{UnivBinders.18} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.18+1,v+1)} +(* u UnivBinders.18 v |= *) Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) @@ -68,19 +68,19 @@ mono The command has indeed failed with message: Universe u already exists. bobmorane = -let tt := Type@{UnivBinders.33} in -let ff := Type@{UnivBinders.35} in tt -> ff - : Type@{max(UnivBinders.32,UnivBinders.34)} +let tt := Type@{UnivBinders.34} in +let ff := Type@{UnivBinders.36} in tt -> ff + : Type@{max(UnivBinders.33,UnivBinders.35)} The command has indeed failed with message: Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) -foo@{u UnivBinders.17 v} = -Type@{UnivBinders.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,UnivBinders.17+1,v+1)} -(* u UnivBinders.17 v |= *) +foo@{u UnivBinders.18 v} = +Type@{UnivBinders.18} -> Type@{v} -> Type@{u} + : Type@{max(u+1,UnivBinders.18+1,v+1)} +(* u UnivBinders.18 v |= *) Inductive Empty@{E} : Type@{E} := (* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -143,16 +143,16 @@ Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) -axfoo@{i UnivBinders.57 UnivBinders.58} : -Type@{UnivBinders.57} -> Type@{i} -(* i UnivBinders.57 UnivBinders.58 |= *) +axfoo@{i UnivBinders.59 UnivBinders.60} : +Type@{UnivBinders.59} -> Type@{i} +(* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.57 UnivBinders.58} : -Type@{UnivBinders.58} -> Type@{i} -(* i UnivBinders.57 UnivBinders.58 |= *) +axbar@{i UnivBinders.59 UnivBinders.60} : +Type@{UnivBinders.60} -> Type@{i} +(* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic Argument scope is [type_scope] diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index adb416e3ce..ab180769b6 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -127,7 +127,6 @@ module Options = struct let all_opts = [ { enabled = false; cmd = "-debug"; } ; { enabled = false; cmd = "-native_compiler"; } - ; { enabled = true; cmd = "-allow-sprop"; } ; { enabled = true; cmd = "-w +default"; } ] diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index acbd96f699..1529959cc6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -113,7 +113,7 @@ let default_logic_config = { impredicative_set = Declarations.PredicativeSet; indices_matter = false; toplevel_name = Stm.TopLogical default_toplevel; - allow_sprop = false; + allow_sprop = true; cumulative_sprop = false; } diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8555d78156..b17ca71f4c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -79,6 +79,7 @@ let print_usage_common co command = \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ \n -allow-sprop allow using the proof irrelevant SProp sort\ +\n -disallow-sprop forbid using the proof irrelevant SProp sort\ \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8cf5e3a8b4..5ba8b0ab3c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -247,8 +247,10 @@ let context_nosection sigma ~poly ctx = let entry = Declare.definition_entry ~univs ~types:t b in Declare.DefinitionEntry entry in - (* let local = Declare.ImportNeedQualified in *) - let cst = Declare.declare_constant ~name ~kind ~local:Declare.ImportNeedQualified decl in + let local = if Lib.is_modtype () then Declare.ImportDefaultBehavior + else Declare.ImportNeedQualified + in + let cst = Declare.declare_constant ~name ~kind ~local decl in let () = Declare.assumption_message name in let env = Global.env () in (* why local when is_modtype? *) |