From 27c8e30fad95d887b698b0e3fa563644c293b033 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 23 Jun 2016 15:07:02 +0200 Subject: Prelude : no more autoload of plugins extraction and recdef The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. --- Makefile.dev | 2 +- doc/refman/Extraction.tex | 7 +++++++ doc/refman/RefMan-ext.tex | 10 ++++++---- doc/refman/RefMan-sch.tex | 7 +++++-- doc/refman/RefMan-tac.tex | 5 ++++- plugins/extraction/ExtrHaskellBasic.v | 2 ++ plugins/extraction/ExtrHaskellNatInt.v | 2 ++ plugins/extraction/ExtrHaskellNatInteger.v | 2 ++ plugins/extraction/ExtrHaskellNatNum.v | 2 ++ plugins/extraction/ExtrHaskellString.v | 2 ++ plugins/extraction/ExtrHaskellZInt.v | 2 ++ plugins/extraction/ExtrHaskellZInteger.v | 2 ++ plugins/extraction/ExtrHaskellZNum.v | 2 ++ plugins/extraction/ExtrOcamlBasic.v | 2 ++ plugins/extraction/ExtrOcamlBigIntConv.v | 2 ++ plugins/extraction/ExtrOcamlIntConv.v | 2 ++ plugins/extraction/ExtrOcamlNatBigInt.v | 2 ++ plugins/extraction/ExtrOcamlNatInt.v | 2 ++ plugins/extraction/ExtrOcamlString.v | 2 ++ plugins/extraction/ExtrOcamlZBigInt.v | 2 ++ plugins/extraction/ExtrOcamlZInt.v | 2 ++ plugins/extraction/Extraction.v | 9 +++++++++ plugins/funind/FunInd.v | 10 ++++++++++ plugins/funind/Recdef.v | 2 +- plugins/micromega/MExtraction.v | 1 + test-suite/bugs/closed/2141.v | 1 + test-suite/bugs/closed/3287.v | 2 ++ test-suite/bugs/closed/3923.v | 2 ++ test-suite/bugs/closed/4616.v | 2 ++ test-suite/bugs/closed/4710.v | 2 ++ test-suite/bugs/closed/5372.v | 1 + test-suite/ide/blocking-futures.fake | 1 + test-suite/output/Extraction_matchs_2413.v | 2 ++ test-suite/success/Funind.v | 2 ++ test-suite/success/RecTutorial.v | 1 + test-suite/success/extraction.v | 1 + test-suite/success/extraction_dep.v | 2 ++ test-suite/success/extraction_impl.v | 2 ++ test-suite/success/extraction_polyprop.v | 2 ++ test-suite/success/primitiveproj.v | 2 ++ theories/Compat/Coq85.v | 3 +++ theories/FSets/FMapAVL.v | 2 +- theories/FSets/FMapFullAVL.v | 2 +- theories/FSets/FMapList.v | 2 +- theories/FSets/FMapWeakList.v | 2 +- theories/Init/Prelude.v | 2 -- theories/MSets/MSetAVL.v | 2 +- theories/MSets/MSetGenTree.v | 2 +- theories/Program/Wf.v | 1 + 49 files changed, 111 insertions(+), 17 deletions(-) create mode 100644 plugins/extraction/Extraction.v create mode 100644 plugins/funind/FunInd.v diff --git a/Makefile.dev b/Makefile.dev index 0105df972a..b0299bd160 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -186,7 +186,7 @@ omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) -extraction: $(EXTRACTIONCMO) +extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) fourier: $(FOURIERVO) $(FOURIERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 01dbcfb1cb..fa3d61b1cd 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -19,6 +19,12 @@ be used (abusively) to refer to any of the three. %% the one in previous versions of \Coq: there is no more %% an explicit toplevel for the language (formerly called \textsc{Fml}). +Before using any of the commands or options described in this chapter, +the extraction framework should first be loaded explicitly +via {\tt Require Extraction}. Note that in earlier versions of Coq, these +commands and options were directly available without any preliminary +{\tt Require}. + \asection{Generating ML code} \comindex{Extraction} \comindex{Recursive Extraction} @@ -501,6 +507,7 @@ We can now extract this program to \ocaml: Reset Initial. \end{coq_eval} \begin{coq_example} +Require Extraction. Require Import Euclid Wf_nat. Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2. Recursive Extraction eucl_dev. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 6dd0ddf81d..939fc87a6e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -721,18 +721,20 @@ a given type. See Section~\ref{Show}. \section{Advanced recursive functions} -The \emph{experimental} command +The following \emph{experimental} command is available +when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: \begin{center} \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} \{decrease\_annot\} : type$_0$ := \term$_0$} \comindex{Function} \label{Function} \end{center} -can be seen as a generalization of {\tt Fixpoint}. It is actually a -wrapper for several ways of defining a function \emph{and other useful +This command can be seen as a generalization of {\tt Fixpoint}. It is actually +a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the recursive structure of the function (see \ref{FunInduction}), and its -fixpoint equality. The meaning of this +fixpoint equality. + The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be given (unless the function is not recursive), but it must not diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 53aa6b86ab..d3719bed46 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -196,8 +196,10 @@ Check tree_forest_mutind. The {\tt Functional Scheme} command is a high-level experimental tool for generating automatically induction principles -corresponding to (possibly mutually recursive) functions. Its -syntax follows the schema: +corresponding to (possibly mutually recursive) functions. +First, it must be made available via {\tt Require Import FunInd}. + Its +syntax then follows the schema: \begin{quote} {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ with\\ @@ -319,6 +321,7 @@ of a tree or a forest. Note that we use \texttt{Function} which generally produces better principles. \begin{coq_example*} +Require Import FunInd. Function tree_size (t:tree) : nat := match t with | node A f => S (forest_size f) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 253eb7f01b..2bab04e90a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2113,13 +2113,15 @@ The tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} -(see Section~\ref{FunScheme}). +(see Section~\ref{FunScheme}). Note that this tactic is only available +after a {\tt Require Import FunInd}. \begin{coq_eval} Reset Initial. Import Nat. \end{coq_eval} \begin{coq_example} +Require Import FunInd. Functional Scheme minus_ind := Induction for minus Sort Prop. Check minus_ind. Lemma le_minus (n m:nat) : n - m <= n. @@ -4797,6 +4799,7 @@ that performs inversion on hypothesis {\ident} of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been defined using \texttt{Function} (see Section~\ref{Function}). +Note that this tactic is only available after a {\tt Require Import FunInd}. \begin{ErrMsgs} \item \errindex{Hypothesis {\ident} must contain at least one Function} diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v index 294d61023b..d08a81da64 100644 --- a/plugins/extraction/ExtrHaskellBasic.v +++ b/plugins/extraction/ExtrHaskellBasic.v @@ -1,5 +1,7 @@ (** Extraction to Haskell : use of basic Haskell types *) +Require Coq.extraction.Extraction. + Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. Extract Inductive unit => "()" [ "()" ]. diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v index e94e7d42bd..267322d9ed 100644 --- a/plugins/extraction/ExtrHaskellNatInt.v +++ b/plugins/extraction/ExtrHaskellNatInt.v @@ -1,5 +1,7 @@ (** Extraction of [nat] into Haskell's [Int] *) +Require Coq.extraction.Extraction. + Require Import Arith. Require Import ExtrHaskellNatNum. diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v index 038f0ed817..4c5c71f58a 100644 --- a/plugins/extraction/ExtrHaskellNatInteger.v +++ b/plugins/extraction/ExtrHaskellNatInteger.v @@ -1,5 +1,7 @@ (** Extraction of [nat] into Haskell's [Integer] *) +Require Coq.extraction.Extraction. + Require Import Arith. Require Import ExtrHaskellNatNum. diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 244eb85fc2..fabe9a4c67 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -6,6 +6,8 @@ * implements [Num]. *) +Require Coq.extraction.Extraction. + Require Import Arith. Require Import EqNat. diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v index 3558f4f254..ac1f6f9130 100644 --- a/plugins/extraction/ExtrHaskellString.v +++ b/plugins/extraction/ExtrHaskellString.v @@ -2,6 +2,8 @@ * Special handling of ascii and strings for extraction to Haskell. *) +Require Coq.extraction.Extraction. + Require Import Ascii. Require Import String. diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v index 66690851a7..0345ffc4e8 100644 --- a/plugins/extraction/ExtrHaskellZInt.v +++ b/plugins/extraction/ExtrHaskellZInt.v @@ -1,5 +1,7 @@ (** Extraction of [Z] into Haskell's [Int] *) +Require Coq.extraction.Extraction. + Require Import ZArith. Require Import ExtrHaskellZNum. diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v index f192f16ee8..f7f9e2f80d 100644 --- a/plugins/extraction/ExtrHaskellZInteger.v +++ b/plugins/extraction/ExtrHaskellZInteger.v @@ -1,5 +1,7 @@ (** Extraction of [Z] into Haskell's [Integer] *) +Require Coq.extraction.Extraction. + Require Import ZArith. Require Import ExtrHaskellZNum. diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v index cbbfda75e5..4141bd203f 100644 --- a/plugins/extraction/ExtrHaskellZNum.v +++ b/plugins/extraction/ExtrHaskellZNum.v @@ -6,6 +6,8 @@ * implements [Num]. *) +Require Coq.extraction.Extraction. + Require Import ZArith. Require Import EqNat. diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index d9b000c2af..dfdc498638 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Coq.extraction.Extraction. + (** Extraction to Ocaml : use of basic Ocaml types *) Extract Inductive bool => bool [ true false ]. diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index c42938c8ec..78ee460856 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -13,6 +13,8 @@ simplifies the use of [Big_int] (it can be found in the sources of Coq). *) +Require Coq.extraction.Extraction. + Require Import Arith ZArith. Parameter bigint : Type. diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index 515fa52dfa..fcfea352a7 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -10,6 +10,8 @@ Nota: no check that [int] values aren't generating overflows *) +Require Coq.extraction.Extraction. + Require Import Arith ZArith. Parameter int : Type. diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 3149e70298..e0837be621 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -8,6 +8,8 @@ (** Extraction of [nat] into Ocaml's [big_int] *) +Require Coq.extraction.Extraction. + Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 7c607f7ae6..80da72d43f 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -8,6 +8,8 @@ (** Extraction of [nat] into Ocaml's [int] *) +Require Coq.extraction.Extraction. + Require Import Arith Even Div2 EqNat Euclid. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 6af591eed3..64ca6c85d0 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -8,6 +8,8 @@ (* Extraction to Ocaml : special handling of ascii and strings *) +Require Coq.extraction.Extraction. + Require Import Ascii String. Extract Inductive ascii => char diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index c9e8eac0c5..66f188c84e 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -8,6 +8,8 @@ (** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *) +Require Coq.extraction.Extraction. + Require Import ZArith NArith. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 4d33174b35..c93cfb9d46 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -8,6 +8,8 @@ (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *) +Require Coq.extraction.Extraction. + Require Import ZArith NArith. Require Import ExtrOcamlBasic. diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v new file mode 100644 index 0000000000..ab1416b1d6 --- /dev/null +++ b/plugins/extraction/Extraction.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* false diff --git a/test-suite/ide/blocking-futures.fake b/test-suite/ide/blocking-futures.fake index b63f09bcfc..541fb798c0 100644 --- a/test-suite/ide/blocking-futures.fake +++ b/test-suite/ide/blocking-futures.fake @@ -4,6 +4,7 @@ # Extraction will force the future computation, assert it is blocking # Example courtesy of Jonathan (jonikelee) # +ADD { Require Coq.extraction.Extraction. } ADD { Require Import List. } ADD { Import ListNotations. } ADD { Definition myrev{A}(l : list A) : {rl : list A | rl = rev l}. } diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v index 6c514b16ee..1ecd9771eb 100644 --- a/test-suite/output/Extraction_matchs_2413.v +++ b/test-suite/output/Extraction_matchs_2413.v @@ -1,5 +1,7 @@ (** Extraction : tests of optimizations of pattern matching *) +Require Coq.extraction.Extraction. + (** First, a few basic tests *) Definition test1 b := diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 3bf97c1312..f87f2e2a9d 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -1,4 +1,6 @@ +Require Import Coq.funind.FunInd. + Definition iszero (n : nat) : bool := match n with | O => true diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index d8f8042465..8419404925 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -147,6 +147,7 @@ Proof. intros; absurd (p < p); eauto with arith. Qed. +Require Coq.extraction.Extraction. Extraction max. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0086e090bd..89be144152 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Coq.extraction.Extraction. Require Import Arith. Require Import List. diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index 11bb25fda0..e770cf779a 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -1,6 +1,8 @@ (** Examples of code elimination inside modules during extraction *) +Require Coq.extraction.Extraction. + (** NB: we should someday check the produced code instead of simply running the commands. *) diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v index dfdeff82ff..5bf807b1c6 100644 --- a/test-suite/success/extraction_impl.v +++ b/test-suite/success/extraction_impl.v @@ -4,6 +4,8 @@ (** NB: we should someday check the produced code instead of simply running the commands. *) +Require Coq.extraction.Extraction. + (** Bug #4243, part 1 *) Inductive dnat : nat -> Type := diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v index 7215bd9905..936d838c50 100644 --- a/test-suite/success/extraction_polyprop.v +++ b/test-suite/success/extraction_polyprop.v @@ -3,6 +3,8 @@ code that segfaults. See Table.error_singleton_become_prop or S. Glondu's thesis for more details. *) +Require Coq.extraction.Extraction. + Definition f {X} (p : (nat -> X) * True) : X * nat := (fst p 0, 0). diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 2fa7704941..789854b2d6 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -181,6 +181,8 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }. Definition term (x : wrap nat) := x.(unwrap). Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. + +Require Coq.extraction.Extraction. Recursive Extraction term term'. (*Unset Printing Primitive Projection Parameters.*) diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 64ba6b1e30..b30ad1af88 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -34,3 +34,6 @@ Global Unset Typeclasses Filtered Unification. (** Allow silently letting unification constraints float after a "." *) Global Unset Solve Unification Constraints. + +Require Export Coq.extraction.Extraction. +Require Export Coq.funind.FunInd. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index c9e5b8dd20..4a790296bb 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -16,7 +16,7 @@ See the comments at the beginning of FSetAVL for more details. *) -Require Import FMapInterface FMapList ZArith Int. +Require Import FunInd FMapInterface FMapList ZArith Int. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index a7be32328d..b8e362f159 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -25,7 +25,7 @@ *) -Require Import Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. +Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 5acdb7eb7e..aadef476d7 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -12,7 +12,7 @@ [FMapInterface.S] using lists of pairs ordered (increasing) with respect to left projection. *) -Require Import FMapInterface. +Require Import FunInd FMapInterface. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 130cbee871..8124097020 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -11,7 +11,7 @@ (** This file proposes an implementation of the non-dependent interface [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) -Require Import FMapInterface. +Require Import FunInd FMapInterface. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index e71a8774ed..28049e9ee5 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -18,9 +18,7 @@ Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. (* Initially available plugins (+ nat_syntax_plugin loaded in Datatypes) *) -Declare ML Module "extraction_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". -Declare ML Module "recdef_plugin". (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index a3c265a21f..b30cb6b565 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -31,7 +31,7 @@ code after extraction. *) -Require Import MSetInterface MSetGenTree BinInt Int. +Require Import FunInd MSetInterface MSetGenTree BinInt Int. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 154c2384c8..036ff1aa4b 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -27,7 +27,7 @@ - min_elt max_elt choose *) -Require Import Orders OrdersFacts MSetInterface PeanoNat. +Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat. Local Open Scope list_scope. Local Open Scope lazy_bool_scope. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index c490ea5166..6e51f61873 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -69,6 +69,7 @@ Section Well_founded. End Well_founded. +Require Coq.extraction.Extraction. Extraction Inline Fix_F_sub Fix_sub. Set Implicit Arguments. -- cgit v1.2.3 From 706b16c3c714f91bfff33ce340aec6f2d24fe246 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 10 Jun 2017 15:54:31 +0200 Subject: API: exports Mltop.module_is_known to both API.mli and grammar_API.mli --- API/API.mli | 1 + API/grammar_API.mli | 1 + 2 files changed, 2 insertions(+) diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..9714f52b91 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3307,6 +3307,7 @@ sig val declare_cache_obj : (unit -> unit) -> string -> unit val add_known_plugin : (unit -> unit) -> string -> unit val add_known_module : string -> unit + val module_is_known : string -> bool end (* All items in the Proof_type module are deprecated. *) diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 44aae771f6..4da5b380fe 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -211,6 +211,7 @@ end module Mltop : sig val add_known_module : string -> unit + val module_is_known : string -> bool val declare_cache_obj : (unit -> unit) -> string -> unit end module Vernacinterp : -- cgit v1.2.3 From a4faac6d24d28ae49ff38477f92f85aef6759075 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 23 Jun 2016 15:11:16 +0200 Subject: Grammar hacks to get nice errors about non-loaded plugins (extr,recdef) Since previous commit, some plugins are not loaded initially anymore : extraction, funind. To ease this transition toward a mandatory Require, we hack here the vernac grammar in order to get customized error messages telling what to Require instead of the dreadful "Illegal begin of vernac". Normally, these fake grammar entries are overloaded later by the grammar extensions in these plugins. This code is meant to be removed in a few releases, when this transition is considered finished. NB : In a first attempt, a similar trick was tried in g_tactics.ml4 to provide customized error message for "functional induction" and "functional inversion", but this was leading to anomalies. --- parsing/g_vernac.ml4 | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 893605499c..b605a44c87 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,6 +51,20 @@ let make_bullet s = | '*' -> Star n | _ -> assert false +let extraction_err ~loc = + if not (Mltop.module_is_known "extraction_plugin") then + CErrors.user_err ~loc (str "Please do first a Require Extraction.") + else + (* The right grammar entries should have been loaded. + We could only end here in case of syntax error. *) + raise (Stream.Error "unexpected end of command") + +let funind_err ~loc = + if not (Mltop.module_is_known "recdef_plugin") then + CErrors.user_err ~loc (str "Please do first a Require Import FunInd.") + else + raise (Stream.Error "unexpected end of command") (* Same as above... *) + GEXTEND Gram GLOBAL: vernac gallina_ext noedit_mode subprf; vernac: FIRST @@ -841,6 +855,22 @@ GEXTEND Gram | IDENT "DelPath"; dir = ne_string -> VernacRemoveLoadPath dir + (* Some plugins are not loaded initially anymore : extraction, + and funind. To ease this transition toward a mandatory Require, + we hack here the vernac grammar in order to get customized + error messages telling what to Require instead of the dreadful + "Illegal begin of vernac". Normally, these fake grammar entries + are overloaded later by the grammar extensions in these plugins. + This code is meant to be removed in a few releases, when this + transition is considered finished. *) + + | IDENT "Extraction" -> extraction_err ~loc:!@loc + | IDENT "Extract" -> extraction_err ~loc:!@loc + | IDENT "Recursive"; IDENT "Extraction" -> extraction_err ~loc:!@loc + | IDENT "Separate"; IDENT "Extraction" -> extraction_err ~loc:!@loc + | IDENT "Function" -> funind_err ~loc:!@loc + | IDENT "Functional" -> funind_err ~loc:!@loc + (* Type-Checking (pas dans le refman) *) | "Type"; c = lconstr -> VernacGlobalCheck c -- cgit v1.2.3 From 930662915d75af750db7da1043f9feda321095b3 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 13 Jun 2017 12:04:34 +0200 Subject: Recdef do now a Require Export FunInd (better compat) --- plugins/funind/Recdef.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index c6fcd647ff..64f43b8335 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Coq.funind.FunInd. +Require Export Coq.funind.FunInd. Require Import PeanoNat. Require Compare_dec. Require Wf_nat. -- cgit v1.2.3 From c70a21a1c522639138dbcfac53fb2ed96d731d98 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 13 Jun 2017 12:05:04 +0200 Subject: [travis] fix CoLoR by inserting some Require Import FunInd --- dev/ci/ci-color.sh | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 57f569858b..a0a4e0749d 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -18,4 +18,18 @@ sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${C sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v +# Adapt to PR #220 (FunInd not loaded in Prelude anymore) +sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v +sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v +sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v +sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v +sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v +sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v +sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v +sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v +sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v +sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v +sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v +sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v + ( cd ${Color_CI_DIR} && make -j ${NJOBS} ) -- cgit v1.2.3 From bba2186f781695db9d0987758119fde061499fbc Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 13 Jun 2017 12:44:01 +0200 Subject: [travis] fix Software Foundation (one added Require Extraction) --- dev/ci/ci-sf.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 7d23ccad97..23ef41d2dd 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh wget ${sf_CI_TARURL} tar xvfz sf.tgz +sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v + ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) -- cgit v1.2.3 From 2470182ac4bded5c433c8f6bc77eb7b96576dc8d Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 13 Jun 2017 14:48:22 +0200 Subject: [travis] overlays for CompCert and VST (an extra Require Export FunInd) --- dev/ci/ci-user-overlay.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 200d431bcb..62c245b4fe 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -47,3 +47,10 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" Corn_CI_BRANCH=external-bignums Corn_CI_GITURL=https://github.com/letouzey/corn.git fi + +if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then + CompCert_CI_BRANCH=less_init_plugins + CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git + VST_CI_BRANCH=less_init_plugins + VST_CI_GITURL=https://github.com/letouzey/VST.git +fi -- cgit v1.2.3 From bb6dbba6a76f83c7cbac7a1f8d6eaa14da2d3d40 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 13 Jun 2017 15:47:56 +0200 Subject: [travis] overlay for fiat-crypto (a Require Import FunInd) --- dev/ci/ci-user-overlay.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 62c245b4fe..2ecd40416f 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -53,4 +53,6 @@ if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git VST_CI_BRANCH=less_init_plugins VST_CI_GITURL=https://github.com/letouzey/VST.git + fiat_crypto_CI_BRANCH=less_init_plugins + fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git fi -- cgit v1.2.3