The package rpms/gappalib-coq.git has added or updated architecture specific content in
its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/gappalib-coq.git/commit/?id=36e05....
Change:
+%ifarch %{ocaml_native_compiler}
Thanks.
Full change:
============
commit 36e05e3b3aa17fb33b02bc755bd4b60f488acc88
Author: Jerry James <loganjerry(a)gmail.com>
Date: Wed Apr 8 21:15:38 2020 -0600
Version 1.4.3.
Drop -coq811 patch in favor of upstream's solution.
diff --git a/gappalib-coq-coq811.patch b/gappalib-coq-coq811.patch
deleted file mode 100644
index b70b49a..0000000
--- a/gappalib-coq-coq811.patch
+++ /dev/null
@@ -1,411 +0,0 @@
---- a/src/Gappa_round_def.v
-+++ b/src/Gappa_round_def.v
-@@ -110,3 +110,6 @@ Global Notation rndZR := Ztrunc (only pa
- Definition rndNE := ZnearestE.
- Definition rndNA := ZnearestA.
- Typeclasses Transparent rndNE rndNA.
-+
-+Register rndNE as gappa.round_def.rndNE.
-+Register rndNA as gappa.round_def.rndNA.
---- a/src/gappatac.ml
-+++ b/src/gappatac.ml
-@@ -9,11 +9,9 @@
- open Format
- open Util
- open Pp
--open Term
- open Tacmach
- open Names
- open Coqlib
--open Libnames
- open Evarutil
-
- let global_env = ref Environ.empty_env
-@@ -21,8 +19,6 @@ let global_evd = ref Evd.empty
-
- let existential_type evd ex = Evd.existential_type evd ex
-
--open Vars
--open Globnames
- open CErrors
-
- let generalize a = Proofview.V82.of_tactic (Tactics.generalize a)
-@@ -40,8 +36,6 @@ let closed0 t = Vars.closed0 !global_evd
-
- let eq_constr t1 t2 = eq_constr !global_evd t1 t2
-
--IFDEF COQ810 THEN
--
- let pr_constr t =
- let sigma, env = Vernacstate.Proof_global.get_current_context () in
- Printer.pr_econstr_env env sigma t
-@@ -53,37 +47,15 @@ let binder_name = Context.binder_name
- let refine_no_check t gl =
- Refiner.refiner ~check:false (EConstr.Unsafe.to_constr t) gl
-
--ELSE
--
--let pr_constr = Printer.pr_econstr
--
--let constr_of_global = Universes.constr_of_global
--
--let binder_name x = x
--
--let refine_no_check = Tacmach.refine_no_check
--
--END
--
- let map_constr f t =
- EConstr.map !global_evd f t
-
- let keep a = Proofview.V82.of_tactic (Tactics.keep a)
- let convert_concl_no_check a b = Proofview.V82.of_tactic (Tactics.convert_concl_no_check
a b)
-
--IFDEF COQ88 THEN
--let parse_entry e s = Pcoq.Gram.entry_parse e (Pcoq.Gram.parsable s)
--ELSE
- let parse_entry e s = Pcoq.Entry.parse e (Pcoq.Parsable.make s)
--END
-
--let coq_reference t1 t2 =
-- let th = lazy (coq_reference t1 t2) in
-- fun x -> lazy (Lazy.force th x)
--
--let find_reference t1 t2 =
-- let th = lazy (find_reference t1 t2) in
-- fun x -> lazy (Lazy.force th x)
-+let coq_lib_ref n = lazy (lib_ref n)
-
- let is_global c t = is_global (Lazy.force c) t
-
-@@ -142,114 +114,107 @@ type pred =
-
- (** {1 Symbols needed by the tactics} *)
-
--let coq_Logic = coq_reference "Gappa" ["Init"; "Logic"]
--let coq_False = coq_Logic "False"
--let coq_True = coq_Logic "True"
--let coq_eq = coq_Logic "eq"
--let coq_eq_refl = coq_Logic "eq_refl"
--let coq_not = coq_Logic "not"
--let coq_and = coq_Logic "and"
--let coq_or = coq_Logic "or"
-+let coq_False = coq_lib_ref "core.False.type"
-+let coq_True = coq_lib_ref "core.True.type"
-+let coq_eq = coq_lib_ref "core.eq.type"
-+let coq_eq_refl = coq_lib_ref "core.eq.refl"
-+let coq_not = coq_lib_ref "core.not.type"
-+let coq_and = coq_lib_ref "core.and.type"
-+let coq_or = coq_lib_ref "core.or.type"
-
--let coq_ref_Datatypes = coq_reference "Gappa" ["Init";
"Datatypes"]
--let coq_Some = coq_ref_Datatypes "Some"
--let coq_cons = coq_ref_Datatypes "cons"
--let coq_nil = coq_ref_Datatypes "nil"
--let coq_bool = coq_ref_Datatypes "bool"
--let coq_true = coq_ref_Datatypes "true"
-+let coq_Some = coq_lib_ref "core.option.Some"
-+let coq_cons = coq_lib_ref "core.list.cons"
-+let coq_nil = coq_lib_ref "core.list.nil"
-+let coq_bool = coq_lib_ref "core.bool.type"
-+let coq_true = coq_lib_ref "core.bool.true"
-
--let coq_ref_BinNums = coq_reference "Gappa" ["Numbers";
"BinNums"]
--let coq_Z0 = coq_ref_BinNums "Z0"
--let coq_Zpos = coq_ref_BinNums "Zpos"
--let coq_Zneg = coq_ref_BinNums "Zneg"
--let coq_xH = coq_ref_BinNums "xH"
--let coq_xI = coq_ref_BinNums "xI"
--let coq_xO = coq_ref_BinNums "xO"
-+let coq_Z0 = coq_lib_ref "num.Z.Z0"
-+let coq_Zpos = coq_lib_ref "num.Z.Zpos"
-+let coq_Zneg = coq_lib_ref "num.Z.Zneg"
-+let coq_xH = coq_lib_ref "num.pos.xH"
-+let coq_xI = coq_lib_ref "num.pos.xI"
-+let coq_xO = coq_lib_ref "num.pos.xO"
-
--let coq_ref_Rdefinitions = coq_reference "Gappa" ["Reals";
"Rdefinitions"]
--let coq_R = coq_ref_Rdefinitions "R"
--let coq_R0 = coq_ref_Rdefinitions "R0"
--let coq_R1 = coq_ref_Rdefinitions "R1"
--let coq_Rle = coq_ref_Rdefinitions "Rle"
--let coq_Rplus = coq_ref_Rdefinitions "Rplus"
--let coq_Ropp = coq_ref_Rdefinitions "Ropp"
--let coq_Rminus = coq_ref_Rdefinitions "Rminus"
--let coq_Rmult = coq_ref_Rdefinitions "Rmult"
--let coq_Rinv = coq_ref_Rdefinitions "Rinv"
--let coq_Rdiv = coq_ref_Rdefinitions "Rdiv"
--let coq_IZR = coq_ref_Rdefinitions "IZR"
--let coq_Rabs = coq_reference "Gappa" ["Reals";
"Rbasic_fun"] "Rabs"
--let coq_sqrt = coq_reference "Gappa" ["Reals"; "R_sqrt"]
"sqrt"
--let coq_powerRZ = coq_reference "Gappa" ["Reals";
"Rfunctions"] "powerRZ"
-+let coq_R = coq_lib_ref "reals.R.type"
-+let coq_R0 = coq_lib_ref "reals.R.R0"
-+let coq_R1 = coq_lib_ref "reals.R.R1"
-+let coq_Rle = coq_lib_ref "reals.R.Rle"
-+let coq_Rplus = coq_lib_ref "reals.R.Rplus"
-+let coq_Ropp = coq_lib_ref "reals.R.Ropp"
-+let coq_Rminus = coq_lib_ref "reals.R.Rminus"
-+let coq_Rmult = coq_lib_ref "reals.R.Rmult"
-+let coq_Rinv = coq_lib_ref "reals.R.Rinv"
-+let coq_Rdiv = coq_lib_ref "reals.R.Rdiv"
-+let coq_IZR = coq_lib_ref "reals.R.IZR"
-+let coq_Rabs = coq_lib_ref "reals.R.Rabs"
-+let coq_sqrt = coq_lib_ref "reals.R.sqrt"
-+let coq_powerRZ = coq_lib_ref "reals.R.powerRZ"
-
--let coq_radix_val = find_reference "Gappa" ["Flocq";
"Core"; "Zaux"] "radix_val"
-+let coq_convert_tree = coq_lib_ref "gappa.gappa_private.convert_tree"
-+let coq_RTree = coq_lib_ref "gappa.gappa_private.RTree"
-+let coq_rtTrue = coq_lib_ref "gappa.gappa_private.rtTrue"
-+let coq_rtFalse = coq_lib_ref "gappa.gappa_private.rtFalse"
-+let coq_rtAtom = coq_lib_ref "gappa.gappa_private.rtAtom"
-+let coq_rtNot = coq_lib_ref "gappa.gappa_private.rtNot"
-+let coq_rtAnd = coq_lib_ref "gappa.gappa_private.rtAnd"
-+let coq_rtOr = coq_lib_ref "gappa.gappa_private.rtOr"
-+let coq_rtImpl = coq_lib_ref "gappa.gappa_private.rtImpl"
-+let coq_RAtom = coq_lib_ref "gappa.gappa_private.RAtom"
-+let coq_raBound = coq_lib_ref "gappa.gappa_private.raBound"
-+let coq_raRel = coq_lib_ref "gappa.gappa_private.raRel"
-+let coq_raEq = coq_lib_ref "gappa.gappa_private.raEq"
-+let coq_raLe = coq_lib_ref "gappa.gappa_private.raLe"
-+let coq_raGeneric = coq_lib_ref "gappa.gappa_private.raGeneric"
-+let coq_raFormat = coq_lib_ref "gappa.gappa_private.raFormat"
-+let coq_RExpr = coq_lib_ref "gappa.gappa_private.RExpr"
-+let coq_reUnknown = coq_lib_ref "gappa.gappa_private.reUnknown"
-+let coq_reFloat2 = coq_lib_ref "gappa.gappa_private.reFloat2"
-+let coq_reFloat10 = coq_lib_ref "gappa.gappa_private.reFloat10"
-+let coq_reBpow2 = coq_lib_ref "gappa.gappa_private.reBpow2"
-+let coq_reBpow10 = coq_lib_ref "gappa.gappa_private.reBpow10"
-+let coq_rePow2 = coq_lib_ref "gappa.gappa_private.rePow2"
-+let coq_rePow10 = coq_lib_ref "gappa.gappa_private.rePow10"
-+let coq_reInteger = coq_lib_ref "gappa.gappa_private.reInteger"
-+let coq_reBinary = coq_lib_ref "gappa.gappa_private.reBinary"
-+let coq_reUnary = coq_lib_ref "gappa.gappa_private.reUnary"
-+let coq_reRound = coq_lib_ref "gappa.gappa_private.reRound"
-+let coq_mRndDN = coq_lib_ref "gappa.gappa_private.mRndDN"
-+let coq_mRndNA = coq_lib_ref "gappa.gappa_private.mRndNA"
-+let coq_mRndNE = coq_lib_ref "gappa.gappa_private.mRndNE"
-+let coq_mRndUP = coq_lib_ref "gappa.gappa_private.mRndUP"
-+let coq_mRndZR = coq_lib_ref "gappa.gappa_private.mRndZR"
-+let coq_fFloat = coq_lib_ref "gappa.gappa_private.fFloat"
-+let coq_fFloatx = coq_lib_ref "gappa.gappa_private.fFloatx"
-+let coq_fFixed = coq_lib_ref "gappa.gappa_private.fFixed"
-+let coq_boAdd = coq_lib_ref "gappa.gappa_private.boAdd"
-+let coq_boSub = coq_lib_ref "gappa.gappa_private.boSub"
-+let coq_boMul = coq_lib_ref "gappa.gappa_private.boMul"
-+let coq_boDiv = coq_lib_ref "gappa.gappa_private.boDiv"
-+let coq_uoAbs = coq_lib_ref "gappa.gappa_private.uoAbs"
-+let coq_uoNeg = coq_lib_ref "gappa.gappa_private.uoNeg"
-+let coq_uoInv = coq_lib_ref "gappa.gappa_private.uoInv"
-+let coq_uoSqrt = coq_lib_ref "gappa.gappa_private.uoSqrt"
-
--let coq_ref_Gappa_Private = find_reference "Gappa" ["Gappa";
"Gappa_tactic"; "Gappa_Private"]
--let coq_convert_tree = coq_ref_Gappa_Private "convert_tree"
--let coq_RTree = coq_ref_Gappa_Private "RTree"
--let coq_rtTrue = coq_ref_Gappa_Private "rtTrue"
--let coq_rtFalse = coq_ref_Gappa_Private "rtFalse"
--let coq_rtAtom = coq_ref_Gappa_Private "rtAtom"
--let coq_rtNot = coq_ref_Gappa_Private "rtNot"
--let coq_rtAnd = coq_ref_Gappa_Private "rtAnd"
--let coq_rtOr = coq_ref_Gappa_Private "rtOr"
--let coq_rtImpl = coq_ref_Gappa_Private "rtImpl"
--let coq_RAtom = coq_ref_Gappa_Private "RAtom"
--let coq_raBound = coq_ref_Gappa_Private "raBound"
--let coq_raRel = coq_ref_Gappa_Private "raRel"
--let coq_raEq = coq_ref_Gappa_Private "raEq"
--let coq_raLe = coq_ref_Gappa_Private "raLe"
--let coq_raGeneric = coq_ref_Gappa_Private "raGeneric"
--let coq_raFormat = coq_ref_Gappa_Private "raFormat"
--let coq_RExpr = coq_ref_Gappa_Private "RExpr"
--let coq_reUnknown = coq_ref_Gappa_Private "reUnknown"
--let coq_reFloat2 = coq_ref_Gappa_Private "reFloat2"
--let coq_reFloat10 = coq_ref_Gappa_Private "reFloat10"
--let coq_reBpow2 = coq_ref_Gappa_Private "reBpow2"
--let coq_reBpow10 = coq_ref_Gappa_Private "reBpow10"
--let coq_rePow2 = coq_ref_Gappa_Private "rePow2"
--let coq_rePow10 = coq_ref_Gappa_Private "rePow10"
--let coq_reInteger = coq_ref_Gappa_Private "reInteger"
--let coq_reBinary = coq_ref_Gappa_Private "reBinary"
--let coq_reUnary = coq_ref_Gappa_Private "reUnary"
--let coq_reRound = coq_ref_Gappa_Private "reRound"
--let coq_mRndDN = coq_ref_Gappa_Private "mRndDN"
--let coq_mRndNA = coq_ref_Gappa_Private "mRndNA"
--let coq_mRndNE = coq_ref_Gappa_Private "mRndNE"
--let coq_mRndUP = coq_ref_Gappa_Private "mRndUP"
--let coq_mRndZR = coq_ref_Gappa_Private "mRndZR"
--let coq_fFloat = coq_ref_Gappa_Private "fFloat"
--let coq_fFloatx = coq_ref_Gappa_Private "fFloatx"
--let coq_fFixed = coq_ref_Gappa_Private "fFixed"
--let coq_boAdd = coq_ref_Gappa_Private "boAdd"
--let coq_boSub = coq_ref_Gappa_Private "boSub"
--let coq_boMul = coq_ref_Gappa_Private "boMul"
--let coq_boDiv = coq_ref_Gappa_Private "boDiv"
--let coq_uoAbs = coq_ref_Gappa_Private "uoAbs"
--let coq_uoNeg = coq_ref_Gappa_Private "uoNeg"
--let coq_uoInv = coq_ref_Gappa_Private "uoInv"
--let coq_uoSqrt = coq_ref_Gappa_Private "uoSqrt"
-+let coq_rndNE = coq_lib_ref "gappa.round_def.rndNE"
-+let coq_rndNA = coq_lib_ref "gappa.round_def.rndNA"
-
--let coq_ref_Fcore_Raux = find_reference "Gappa" ["Flocq";
"Core"; "Raux"]
--let coq_bpow = coq_ref_Fcore_Raux "bpow"
--let coq_rndDN = coq_ref_Fcore_Raux "Zfloor"
--let coq_rndUP = coq_ref_Fcore_Raux "Zceil"
--let coq_rndZR = coq_ref_Fcore_Raux "Ztrunc"
--let coq_ref_Gappa_round_def = find_reference "Gappa" ["Gappa";
"Gappa_round_def"]
--let coq_rndNE = coq_ref_Gappa_round_def "rndNE"
--let coq_rndNA = coq_ref_Gappa_round_def "rndNA"
--let coq_ref_Fcore_generic_fmt = find_reference "Gappa" ["Flocq";
"Core"; "Generic_fmt"]
--let coq_round = coq_ref_Fcore_generic_fmt "round"
--let coq_generic_format = coq_ref_Fcore_generic_fmt "generic_format"
--let coq_ref_Fcore_FLT = find_reference "Gappa" ["Flocq";
"Core"; "FLT"]
--let coq_FLT_format = coq_ref_Fcore_FLT "FLT_format"
--let coq_FLT_exp = coq_ref_Fcore_FLT "FLT_exp"
--let coq_ref_Fcore_FLX = find_reference "Gappa" ["Flocq";
"Core"; "FLX"]
--let coq_FLX_format = coq_ref_Fcore_FLX "FLX_format"
--let coq_FLX_exp = coq_ref_Fcore_FLX "FLX_exp"
--let coq_ref_Fcore_FIX = find_reference "Gappa" ["Flocq";
"Core"; "FIX"]
--let coq_FIX_format = coq_ref_Fcore_FIX "FIX_format"
--let coq_FIX_exp = coq_ref_Fcore_FIX "FIX_exp"
-+let coq_radix_val = coq_lib_ref "flocq.zaux.radix_val"
-+let coq_bpow = coq_lib_ref "flocq.raux.bpow"
-+let coq_rndDN = coq_lib_ref "flocq.raux.Zfloor"
-+let coq_rndUP = coq_lib_ref "flocq.raux.Zceil"
-+let coq_rndZR = coq_lib_ref "flocq.raux.Ztrunc"
-+
-+let coq_round = coq_lib_ref "flocq.generic_fmt.round"
-+let coq_generic_format = coq_lib_ref "flocq.generic_fmt.generic_format"
-+
-+let coq_FLT_format = coq_lib_ref "flocq.flt.FLT_format"
-+let coq_FLT_exp = coq_lib_ref "flocq.flt.FLT_exp"
-+
-+let coq_FLX_format = coq_lib_ref "flocq.flx.FLX_format"
-+let coq_FLX_exp = coq_lib_ref "flocq.flx.FLX_exp"
-+
-+let coq_FIX_format = coq_lib_ref "flocq.fix.FIX_format"
-+let coq_FIX_exp = coq_lib_ref "flocq.fix.FIX_exp"
-
- (** {1 Reification from Coq user goal: the [gappa_quote] tactic} *)
-
---- a/src/Gappa_tactic.v
-+++ b/src/Gappa_tactic.v
-@@ -69,14 +69,28 @@ Qed.
- Inductive UnaryOp : Set :=
- | uoNeg | uoSqrt | uoAbs | uoInv.
-
-+Register uoAbs as gappa.gappa_private.uoAbs.
-+Register uoNeg as gappa.gappa_private.uoNeg.
-+Register uoInv as gappa.gappa_private.uoInv.
-+Register uoSqrt as gappa.gappa_private.uoSqrt.
-+
- Inductive BinaryOp : Set :=
- | boAdd | boSub | boMul | boDiv.
-
-+Register boAdd as gappa.gappa_private.boAdd.
-+Register boSub as gappa.gappa_private.boSub.
-+Register boMul as gappa.gappa_private.boMul.
-+Register boDiv as gappa.gappa_private.boDiv.
-+
- Inductive Format : Set :=
- | fFixed : Z -> Format
- | fFloat : Z -> Z -> Format
- | fFloatx : Z -> Format.
-
-+Register fFloat as gappa.gappa_private.fFloat.
-+Register fFloatx as gappa.gappa_private.fFloatx.
-+Register fFixed as gappa.gappa_private.fFixed.
-+
- Inductive Mode : Set :=
- | mRndDN
- | mRndUP
-@@ -84,6 +98,12 @@ Inductive Mode : Set :=
- | mRndNE
- | mRndNA.
-
-+Register mRndDN as gappa.gappa_private.mRndDN.
-+Register mRndUP as gappa.gappa_private.mRndUP.
-+Register mRndZR as gappa.gappa_private.mRndZR.
-+Register mRndNE as gappa.gappa_private.mRndNE.
-+Register mRndNA as gappa.gappa_private.mRndNA.
-+
- (* represent an expression on real numbers *)
- Inductive RExpr :=
- | reUnknown : positive -> RExpr
-@@ -100,6 +120,19 @@ Inductive RExpr :=
- | reIZR : Z -> RExpr
- | reRound : Format -> Mode -> RExpr -> RExpr.
-
-+Register RExpr as gappa.gappa_private.RExpr.
-+Register reUnknown as gappa.gappa_private.reUnknown.
-+Register reInteger as gappa.gappa_private.reInteger.
-+Register reFloat2 as gappa.gappa_private.reFloat2.
-+Register reFloat10 as gappa.gappa_private.reFloat10.
-+Register reUnary as gappa.gappa_private.reUnary.
-+Register reBinary as gappa.gappa_private.reBinary.
-+Register reBpow2 as gappa.gappa_private.reBpow2.
-+Register reBpow10 as gappa.gappa_private.reBpow10.
-+Register rePow2 as gappa.gappa_private.rePow2.
-+Register rePow10 as gappa.gappa_private.rePow10.
-+Register reRound as gappa.gappa_private.reRound.
-+
- Scheme Equality for positive.
- Scheme Equality for Z.
- Scheme Equality for UnaryOp.
-@@ -117,6 +150,14 @@ Inductive RAtom :=
- | raGeneric : Format -> RExpr -> RAtom
- | raFormat : Format -> RExpr -> RAtom.
-
-+Register RAtom as gappa.gappa_private.RAtom.
-+Register raBound as gappa.gappa_private.raBound.
-+Register raRel as gappa.gappa_private.raRel.
-+Register raEq as gappa.gappa_private.raEq.
-+Register raLe as gappa.gappa_private.raLe.
-+Register raGeneric as gappa.gappa_private.raGeneric.
-+Register raFormat as gappa.gappa_private.raFormat.
-+
- Inductive RTree :=
- | rtTrue : RTree
- | rtFalse : RTree
-@@ -126,6 +167,15 @@ Inductive RTree :=
- | rtOr : RTree -> RTree -> RTree
- | rtImpl : RTree -> RTree -> RTree.
-
-+Register RTree as gappa.gappa_private.RTree.
-+Register rtTrue as gappa.gappa_private.rtTrue.
-+Register rtFalse as gappa.gappa_private.rtFalse.
-+Register rtAtom as gappa.gappa_private.rtAtom.
-+Register rtNot as gappa.gappa_private.rtNot.
-+Register rtAnd as gappa.gappa_private.rtAnd.
-+Register rtOr as gappa.gappa_private.rtOr.
-+Register rtImpl as gappa.gappa_private.rtImpl.
-+
- Section Convert.
-
- Definition convert_exp (f : Format) : Z -> Z :=
-@@ -216,6 +266,8 @@ Fixpoint convert_tree (t : RTree) : Prop
- | rtImpl t1 t2 => (convert_tree t1) -> (convert_tree t2)
- end.
-
-+Register convert_tree as gappa.gappa_private.convert_tree.
-+
- Lemma decidable_atom :
- forall a, { convert_atom a } + { not (convert_atom a) }.
- Proof with auto with typeclass_instances.
-@@ -1136,7 +1188,7 @@ Definition trans :=
- trLeaf change_format_func change_format_prop ::
- trLeaf remove_unknown_func remove_unknown_prop ::
- trTree simplify_tree simplify_tree_correct ::
-- nil.
-+ List.nil.
-
- Theorem prepare_goal :
- forall uv t,
-@@ -1181,4 +1233,7 @@ Ltac gappa_prepare :=
- convert_apply ltac:(fun uv g => refine (prepare_goal uv g _)) ;
- convert_apply ltac:(fun uv g => let g := eval vm_compute in g in change
(convert_tree uv g)).
-
-+Require Rregisternames.
-+Require Flocq.Core.Registernames.
-+
- Ltac gappa := abstract (gappa_prepare ; gappa_internal).
diff --git a/gappalib-coq.spec b/gappalib-coq.spec
index 1b9ec1b..3ae64ea 100644
--- a/gappalib-coq.spec
+++ b/gappalib-coq.spec
@@ -1,4 +1,8 @@
-%ifnarch %{ocaml_native_compiler}
+# On platforms with a native OCaml compiler, proofs can be compiled into cmxs
+# files, but there are no source files that rpm recognizes as such.
+%ifarch %{ocaml_native_compiler}
+%global _debugsource_template %{nil}
+%else
%global debug_package %{nil}
%endif
@@ -10,16 +14,13 @@
%global coqver 8.11.0
Name: gappalib-coq
-Version: 1.4.2
-Release: 6%{?dist}
+Version: 1.4.3
+Release: 1%{?dist}
Summary: Coq support library for gappa
License: LGPLv2+
URL:
http://gappa.gforge.inria.fr/
-Source0:
https://gforge.inria.fr/frs/download.php/file/38102/%{name}-%{version}.ta...
-# Adapt to coq 8.11.0
-#
https://github.com/MSoegtropIMC/gappa-coq/commit/d6f5177181c35f07ff50bd5c...
-Patch0: %{name}-coq811.patch
+Source0:
https://gforge.inria.fr/frs/download.php/file/38302/%{name}-%{version}.ta...
BuildRequires: gcc-c++
BuildRequires: coq = %{coqver}
@@ -27,6 +28,7 @@ BuildRequires: flocq
BuildRequires: gappa
BuildRequires: ocaml
BuildRequires: ocaml-camlp5-devel
+BuildRequires: ocaml-findlib
BuildRequires: remake
Requires: coq%{?_isa} = %{coqver}
@@ -61,6 +63,11 @@ sed -i 's/-pp/-g &/' Remakefile.in
# Workaround broken ocamlopt version detection with beta ocaml versions
sed -i 's/^\(ocamlopt_version=`.*\)\(`\)/\1 | cut -d+ -f1\2/' configure
+# Force native compilation when available
+%ifarch %{ocaml_native_compiler}
+sed -i 's/@COQC@ -R src Gappa/& -native-compiler yes/' Remakefile.in
+%endif
+
%build
# The %%configure macro specifies --libdir, which this configure script
# unfortunately uses to identify where the Coq files should go. We want
@@ -77,6 +84,7 @@ remake -d %{?_smp_mflags}
sed -i '/^install:/,/^EXTRA_DIST/s, /usr, %{buildroot}%{_prefix},' Remakefile
mkdir -p %{buildroot}%{gappadir}
remake install
+cp -a src/.coq-native %{buildroot}%{gappadir}
# Also install the source files
cp -p src/*.v %{buildroot}%{gappadir}
@@ -94,6 +102,10 @@ remake check
%{gappadir}/*.v
%changelog
+* Wed Apr 8 2020 Jerry James <loganjerry(a)gmail.com> - 1.4.3-1
+- Version 1.4.3
+- Drop -coq811 patch in favor of upstream's solution
+
* Mon Mar 30 2020 Jerry James <loganjerry(a)gmail.com> - 1.4.2-6
- Add -coq811 patch to fix the build with coq 8.11
diff --git a/sources b/sources
index e21bb27..8c994fa 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-SHA512 (gappalib-coq-1.4.2.tar.gz) =
60e8c9e1db5ae6d993b5b7af744bb78963ea57cff211a43f98814a1f79d05564d0f2eb6fb9fc263c34f06205f7a2a99bb988a92d1f9f6c379791225909c516e5
+SHA512 (gappalib-coq-1.4.3.tar.gz) =
1a1b45121a2e581b9f7b4060455a496567563f7b75fc88323933b4b10bfd28adc5cb2e3d15aab74ad3d354d921fde2bf534a9498bc4907737ca7aa97054af7e6
commit 7fa73970fba06a2322d21e9ff9d8a64927b4cdb1
Author: Jerry James <loganjerry(a)gmail.com>
Date: Mon Mar 30 10:37:35 2020 -0600
Add -coq811 patch to fix the build with coq 8.11.
diff --git a/gappalib-coq-coq811.patch b/gappalib-coq-coq811.patch
new file mode 100644
index 0000000..b70b49a
--- /dev/null
+++ b/gappalib-coq-coq811.patch
@@ -0,0 +1,411 @@
+--- a/src/Gappa_round_def.v
++++ b/src/Gappa_round_def.v
+@@ -110,3 +110,6 @@ Global Notation rndZR := Ztrunc (only pa
+ Definition rndNE := ZnearestE.
+ Definition rndNA := ZnearestA.
+ Typeclasses Transparent rndNE rndNA.
++
++Register rndNE as gappa.round_def.rndNE.
++Register rndNA as gappa.round_def.rndNA.
+--- a/src/gappatac.ml
++++ b/src/gappatac.ml
+@@ -9,11 +9,9 @@
+ open Format
+ open Util
+ open Pp
+-open Term
+ open Tacmach
+ open Names
+ open Coqlib
+-open Libnames
+ open Evarutil
+
+ let global_env = ref Environ.empty_env
+@@ -21,8 +19,6 @@ let global_evd = ref Evd.empty
+
+ let existential_type evd ex = Evd.existential_type evd ex
+
+-open Vars
+-open Globnames
+ open CErrors
+
+ let generalize a = Proofview.V82.of_tactic (Tactics.generalize a)
+@@ -40,8 +36,6 @@ let closed0 t = Vars.closed0 !global_evd
+
+ let eq_constr t1 t2 = eq_constr !global_evd t1 t2
+
+-IFDEF COQ810 THEN
+-
+ let pr_constr t =
+ let sigma, env = Vernacstate.Proof_global.get_current_context () in
+ Printer.pr_econstr_env env sigma t
+@@ -53,37 +47,15 @@ let binder_name = Context.binder_name
+ let refine_no_check t gl =
+ Refiner.refiner ~check:false (EConstr.Unsafe.to_constr t) gl
+
+-ELSE
+-
+-let pr_constr = Printer.pr_econstr
+-
+-let constr_of_global = Universes.constr_of_global
+-
+-let binder_name x = x
+-
+-let refine_no_check = Tacmach.refine_no_check
+-
+-END
+-
+ let map_constr f t =
+ EConstr.map !global_evd f t
+
+ let keep a = Proofview.V82.of_tactic (Tactics.keep a)
+ let convert_concl_no_check a b = Proofview.V82.of_tactic (Tactics.convert_concl_no_check
a b)
+
+-IFDEF COQ88 THEN
+-let parse_entry e s = Pcoq.Gram.entry_parse e (Pcoq.Gram.parsable s)
+-ELSE
+ let parse_entry e s = Pcoq.Entry.parse e (Pcoq.Parsable.make s)
+-END
+
+-let coq_reference t1 t2 =
+- let th = lazy (coq_reference t1 t2) in
+- fun x -> lazy (Lazy.force th x)
+-
+-let find_reference t1 t2 =
+- let th = lazy (find_reference t1 t2) in
+- fun x -> lazy (Lazy.force th x)
++let coq_lib_ref n = lazy (lib_ref n)
+
+ let is_global c t = is_global (Lazy.force c) t
+
+@@ -142,114 +114,107 @@ type pred =
+
+ (** {1 Symbols needed by the tactics} *)
+
+-let coq_Logic = coq_reference "Gappa" ["Init"; "Logic"]
+-let coq_False = coq_Logic "False"
+-let coq_True = coq_Logic "True"
+-let coq_eq = coq_Logic "eq"
+-let coq_eq_refl = coq_Logic "eq_refl"
+-let coq_not = coq_Logic "not"
+-let coq_and = coq_Logic "and"
+-let coq_or = coq_Logic "or"
++let coq_False = coq_lib_ref "core.False.type"
++let coq_True = coq_lib_ref "core.True.type"
++let coq_eq = coq_lib_ref "core.eq.type"
++let coq_eq_refl = coq_lib_ref "core.eq.refl"
++let coq_not = coq_lib_ref "core.not.type"
++let coq_and = coq_lib_ref "core.and.type"
++let coq_or = coq_lib_ref "core.or.type"
+
+-let coq_ref_Datatypes = coq_reference "Gappa" ["Init";
"Datatypes"]
+-let coq_Some = coq_ref_Datatypes "Some"
+-let coq_cons = coq_ref_Datatypes "cons"
+-let coq_nil = coq_ref_Datatypes "nil"
+-let coq_bool = coq_ref_Datatypes "bool"
+-let coq_true = coq_ref_Datatypes "true"
++let coq_Some = coq_lib_ref "core.option.Some"
++let coq_cons = coq_lib_ref "core.list.cons"
++let coq_nil = coq_lib_ref "core.list.nil"
++let coq_bool = coq_lib_ref "core.bool.type"
++let coq_true = coq_lib_ref "core.bool.true"
+
+-let coq_ref_BinNums = coq_reference "Gappa" ["Numbers";
"BinNums"]
+-let coq_Z0 = coq_ref_BinNums "Z0"
+-let coq_Zpos = coq_ref_BinNums "Zpos"
+-let coq_Zneg = coq_ref_BinNums "Zneg"
+-let coq_xH = coq_ref_BinNums "xH"
+-let coq_xI = coq_ref_BinNums "xI"
+-let coq_xO = coq_ref_BinNums "xO"
++let coq_Z0 = coq_lib_ref "num.Z.Z0"
++let coq_Zpos = coq_lib_ref "num.Z.Zpos"
++let coq_Zneg = coq_lib_ref "num.Z.Zneg"
++let coq_xH = coq_lib_ref "num.pos.xH"
++let coq_xI = coq_lib_ref "num.pos.xI"
++let coq_xO = coq_lib_ref "num.pos.xO"
+
+-let coq_ref_Rdefinitions = coq_reference "Gappa" ["Reals";
"Rdefinitions"]
+-let coq_R = coq_ref_Rdefinitions "R"
+-let coq_R0 = coq_ref_Rdefinitions "R0"
+-let coq_R1 = coq_ref_Rdefinitions "R1"
+-let coq_Rle = coq_ref_Rdefinitions "Rle"
+-let coq_Rplus = coq_ref_Rdefinitions "Rplus"
+-let coq_Ropp = coq_ref_Rdefinitions "Ropp"
+-let coq_Rminus = coq_ref_Rdefinitions "Rminus"
+-let coq_Rmult = coq_ref_Rdefinitions "Rmult"
+-let coq_Rinv = coq_ref_Rdefinitions "Rinv"
+-let coq_Rdiv = coq_ref_Rdefinitions "Rdiv"
+-let coq_IZR = coq_ref_Rdefinitions "IZR"
+-let coq_Rabs = coq_reference "Gappa" ["Reals";
"Rbasic_fun"] "Rabs"
+-let coq_sqrt = coq_reference "Gappa" ["Reals"; "R_sqrt"]
"sqrt"
+-let coq_powerRZ = coq_reference "Gappa" ["Reals";
"Rfunctions"] "powerRZ"
++let coq_R = coq_lib_ref "reals.R.type"
++let coq_R0 = coq_lib_ref "reals.R.R0"
++let coq_R1 = coq_lib_ref "reals.R.R1"
++let coq_Rle = coq_lib_ref "reals.R.Rle"
++let coq_Rplus = coq_lib_ref "reals.R.Rplus"
++let coq_Ropp = coq_lib_ref "reals.R.Ropp"
++let coq_Rminus = coq_lib_ref "reals.R.Rminus"
++let coq_Rmult = coq_lib_ref "reals.R.Rmult"
++let coq_Rinv = coq_lib_ref "reals.R.Rinv"
++let coq_Rdiv = coq_lib_ref "reals.R.Rdiv"
++let coq_IZR = coq_lib_ref "reals.R.IZR"
++let coq_Rabs = coq_lib_ref "reals.R.Rabs"
++let coq_sqrt = coq_lib_ref "reals.R.sqrt"
++let coq_powerRZ = coq_lib_ref "reals.R.powerRZ"
+
+-let coq_radix_val = find_reference "Gappa" ["Flocq";
"Core"; "Zaux"] "radix_val"
++let coq_convert_tree = coq_lib_ref "gappa.gappa_private.convert_tree"
++let coq_RTree = coq_lib_ref "gappa.gappa_private.RTree"
++let coq_rtTrue = coq_lib_ref "gappa.gappa_private.rtTrue"
++let coq_rtFalse = coq_lib_ref "gappa.gappa_private.rtFalse"
++let coq_rtAtom = coq_lib_ref "gappa.gappa_private.rtAtom"
++let coq_rtNot = coq_lib_ref "gappa.gappa_private.rtNot"
++let coq_rtAnd = coq_lib_ref "gappa.gappa_private.rtAnd"
++let coq_rtOr = coq_lib_ref "gappa.gappa_private.rtOr"
++let coq_rtImpl = coq_lib_ref "gappa.gappa_private.rtImpl"
++let coq_RAtom = coq_lib_ref "gappa.gappa_private.RAtom"
++let coq_raBound = coq_lib_ref "gappa.gappa_private.raBound"
++let coq_raRel = coq_lib_ref "gappa.gappa_private.raRel"
++let coq_raEq = coq_lib_ref "gappa.gappa_private.raEq"
++let coq_raLe = coq_lib_ref "gappa.gappa_private.raLe"
++let coq_raGeneric = coq_lib_ref "gappa.gappa_private.raGeneric"
++let coq_raFormat = coq_lib_ref "gappa.gappa_private.raFormat"
++let coq_RExpr = coq_lib_ref "gappa.gappa_private.RExpr"
++let coq_reUnknown = coq_lib_ref "gappa.gappa_private.reUnknown"
++let coq_reFloat2 = coq_lib_ref "gappa.gappa_private.reFloat2"
++let coq_reFloat10 = coq_lib_ref "gappa.gappa_private.reFloat10"
++let coq_reBpow2 = coq_lib_ref "gappa.gappa_private.reBpow2"
++let coq_reBpow10 = coq_lib_ref "gappa.gappa_private.reBpow10"
++let coq_rePow2 = coq_lib_ref "gappa.gappa_private.rePow2"
++let coq_rePow10 = coq_lib_ref "gappa.gappa_private.rePow10"
++let coq_reInteger = coq_lib_ref "gappa.gappa_private.reInteger"
++let coq_reBinary = coq_lib_ref "gappa.gappa_private.reBinary"
++let coq_reUnary = coq_lib_ref "gappa.gappa_private.reUnary"
++let coq_reRound = coq_lib_ref "gappa.gappa_private.reRound"
++let coq_mRndDN = coq_lib_ref "gappa.gappa_private.mRndDN"
++let coq_mRndNA = coq_lib_ref "gappa.gappa_private.mRndNA"
++let coq_mRndNE = coq_lib_ref "gappa.gappa_private.mRndNE"
++let coq_mRndUP = coq_lib_ref "gappa.gappa_private.mRndUP"
++let coq_mRndZR = coq_lib_ref "gappa.gappa_private.mRndZR"
++let coq_fFloat = coq_lib_ref "gappa.gappa_private.fFloat"
++let coq_fFloatx = coq_lib_ref "gappa.gappa_private.fFloatx"
++let coq_fFixed = coq_lib_ref "gappa.gappa_private.fFixed"
++let coq_boAdd = coq_lib_ref "gappa.gappa_private.boAdd"
++let coq_boSub = coq_lib_ref "gappa.gappa_private.boSub"
++let coq_boMul = coq_lib_ref "gappa.gappa_private.boMul"
++let coq_boDiv = coq_lib_ref "gappa.gappa_private.boDiv"
++let coq_uoAbs = coq_lib_ref "gappa.gappa_private.uoAbs"
++let coq_uoNeg = coq_lib_ref "gappa.gappa_private.uoNeg"
++let coq_uoInv = coq_lib_ref "gappa.gappa_private.uoInv"
++let coq_uoSqrt = coq_lib_ref "gappa.gappa_private.uoSqrt"
+
+-let coq_ref_Gappa_Private = find_reference "Gappa" ["Gappa";
"Gappa_tactic"; "Gappa_Private"]
+-let coq_convert_tree = coq_ref_Gappa_Private "convert_tree"
+-let coq_RTree = coq_ref_Gappa_Private "RTree"
+-let coq_rtTrue = coq_ref_Gappa_Private "rtTrue"
+-let coq_rtFalse = coq_ref_Gappa_Private "rtFalse"
+-let coq_rtAtom = coq_ref_Gappa_Private "rtAtom"
+-let coq_rtNot = coq_ref_Gappa_Private "rtNot"
+-let coq_rtAnd = coq_ref_Gappa_Private "rtAnd"
+-let coq_rtOr = coq_ref_Gappa_Private "rtOr"
+-let coq_rtImpl = coq_ref_Gappa_Private "rtImpl"
+-let coq_RAtom = coq_ref_Gappa_Private "RAtom"
+-let coq_raBound = coq_ref_Gappa_Private "raBound"
+-let coq_raRel = coq_ref_Gappa_Private "raRel"
+-let coq_raEq = coq_ref_Gappa_Private "raEq"
+-let coq_raLe = coq_ref_Gappa_Private "raLe"
+-let coq_raGeneric = coq_ref_Gappa_Private "raGeneric"
+-let coq_raFormat = coq_ref_Gappa_Private "raFormat"
+-let coq_RExpr = coq_ref_Gappa_Private "RExpr"
+-let coq_reUnknown = coq_ref_Gappa_Private "reUnknown"
+-let coq_reFloat2 = coq_ref_Gappa_Private "reFloat2"
+-let coq_reFloat10 = coq_ref_Gappa_Private "reFloat10"
+-let coq_reBpow2 = coq_ref_Gappa_Private "reBpow2"
+-let coq_reBpow10 = coq_ref_Gappa_Private "reBpow10"
+-let coq_rePow2 = coq_ref_Gappa_Private "rePow2"
+-let coq_rePow10 = coq_ref_Gappa_Private "rePow10"
+-let coq_reInteger = coq_ref_Gappa_Private "reInteger"
+-let coq_reBinary = coq_ref_Gappa_Private "reBinary"
+-let coq_reUnary = coq_ref_Gappa_Private "reUnary"
+-let coq_reRound = coq_ref_Gappa_Private "reRound"
+-let coq_mRndDN = coq_ref_Gappa_Private "mRndDN"
+-let coq_mRndNA = coq_ref_Gappa_Private "mRndNA"
+-let coq_mRndNE = coq_ref_Gappa_Private "mRndNE"
+-let coq_mRndUP = coq_ref_Gappa_Private "mRndUP"
+-let coq_mRndZR = coq_ref_Gappa_Private "mRndZR"
+-let coq_fFloat = coq_ref_Gappa_Private "fFloat"
+-let coq_fFloatx = coq_ref_Gappa_Private "fFloatx"
+-let coq_fFixed = coq_ref_Gappa_Private "fFixed"
+-let coq_boAdd = coq_ref_Gappa_Private "boAdd"
+-let coq_boSub = coq_ref_Gappa_Private "boSub"
+-let coq_boMul = coq_ref_Gappa_Private "boMul"
+-let coq_boDiv = coq_ref_Gappa_Private "boDiv"
+-let coq_uoAbs = coq_ref_Gappa_Private "uoAbs"
+-let coq_uoNeg = coq_ref_Gappa_Private "uoNeg"
+-let coq_uoInv = coq_ref_Gappa_Private "uoInv"
+-let coq_uoSqrt = coq_ref_Gappa_Private "uoSqrt"
++let coq_rndNE = coq_lib_ref "gappa.round_def.rndNE"
++let coq_rndNA = coq_lib_ref "gappa.round_def.rndNA"
+
+-let coq_ref_Fcore_Raux = find_reference "Gappa" ["Flocq";
"Core"; "Raux"]
+-let coq_bpow = coq_ref_Fcore_Raux "bpow"
+-let coq_rndDN = coq_ref_Fcore_Raux "Zfloor"
+-let coq_rndUP = coq_ref_Fcore_Raux "Zceil"
+-let coq_rndZR = coq_ref_Fcore_Raux "Ztrunc"
+-let coq_ref_Gappa_round_def = find_reference "Gappa" ["Gappa";
"Gappa_round_def"]
+-let coq_rndNE = coq_ref_Gappa_round_def "rndNE"
+-let coq_rndNA = coq_ref_Gappa_round_def "rndNA"
+-let coq_ref_Fcore_generic_fmt = find_reference "Gappa" ["Flocq";
"Core"; "Generic_fmt"]
+-let coq_round = coq_ref_Fcore_generic_fmt "round"
+-let coq_generic_format = coq_ref_Fcore_generic_fmt "generic_format"
+-let coq_ref_Fcore_FLT = find_reference "Gappa" ["Flocq";
"Core"; "FLT"]
+-let coq_FLT_format = coq_ref_Fcore_FLT "FLT_format"
+-let coq_FLT_exp = coq_ref_Fcore_FLT "FLT_exp"
+-let coq_ref_Fcore_FLX = find_reference "Gappa" ["Flocq";
"Core"; "FLX"]
+-let coq_FLX_format = coq_ref_Fcore_FLX "FLX_format"
+-let coq_FLX_exp = coq_ref_Fcore_FLX "FLX_exp"
+-let coq_ref_Fcore_FIX = find_reference "Gappa" ["Flocq";
"Core"; "FIX"]
+-let coq_FIX_format = coq_ref_Fcore_FIX "FIX_format"
+-let coq_FIX_exp = coq_ref_Fcore_FIX "FIX_exp"
++let coq_radix_val = coq_lib_ref "flocq.zaux.radix_val"
++let coq_bpow = coq_lib_ref "flocq.raux.bpow"
++let coq_rndDN = coq_lib_ref "flocq.raux.Zfloor"
++let coq_rndUP = coq_lib_ref "flocq.raux.Zceil"
++let coq_rndZR = coq_lib_ref "flocq.raux.Ztrunc"
++
++let coq_round = coq_lib_ref "flocq.generic_fmt.round"
++let coq_generic_format = coq_lib_ref "flocq.generic_fmt.generic_format"
++
++let coq_FLT_format = coq_lib_ref "flocq.flt.FLT_format"
++let coq_FLT_exp = coq_lib_ref "flocq.flt.FLT_exp"
++
++let coq_FLX_format = coq_lib_ref "flocq.flx.FLX_format"
++let coq_FLX_exp = coq_lib_ref "flocq.flx.FLX_exp"
++
++let coq_FIX_format = coq_lib_ref "flocq.fix.FIX_format"
++let coq_FIX_exp = coq_lib_ref "flocq.fix.FIX_exp"
+
+ (** {1 Reification from Coq user goal: the [gappa_quote] tactic} *)
+
+--- a/src/Gappa_tactic.v
++++ b/src/Gappa_tactic.v
+@@ -69,14 +69,28 @@ Qed.
+ Inductive UnaryOp : Set :=
+ | uoNeg | uoSqrt | uoAbs | uoInv.
+
++Register uoAbs as gappa.gappa_private.uoAbs.
++Register uoNeg as gappa.gappa_private.uoNeg.
++Register uoInv as gappa.gappa_private.uoInv.
++Register uoSqrt as gappa.gappa_private.uoSqrt.
++
+ Inductive BinaryOp : Set :=
+ | boAdd | boSub | boMul | boDiv.
+
++Register boAdd as gappa.gappa_private.boAdd.
++Register boSub as gappa.gappa_private.boSub.
++Register boMul as gappa.gappa_private.boMul.
++Register boDiv as gappa.gappa_private.boDiv.
++
+ Inductive Format : Set :=
+ | fFixed : Z -> Format
+ | fFloat : Z -> Z -> Format
+ | fFloatx : Z -> Format.
+
++Register fFloat as gappa.gappa_private.fFloat.
++Register fFloatx as gappa.gappa_private.fFloatx.
++Register fFixed as gappa.gappa_private.fFixed.
++
+ Inductive Mode : Set :=
+ | mRndDN
+ | mRndUP
+@@ -84,6 +98,12 @@ Inductive Mode : Set :=
+ | mRndNE
+ | mRndNA.
+
++Register mRndDN as gappa.gappa_private.mRndDN.
++Register mRndUP as gappa.gappa_private.mRndUP.
++Register mRndZR as gappa.gappa_private.mRndZR.
++Register mRndNE as gappa.gappa_private.mRndNE.
++Register mRndNA as gappa.gappa_private.mRndNA.
++
+ (* represent an expression on real numbers *)
+ Inductive RExpr :=
+ | reUnknown : positive -> RExpr
+@@ -100,6 +120,19 @@ Inductive RExpr :=
+ | reIZR : Z -> RExpr
+ | reRound : Format -> Mode -> RExpr -> RExpr.
+
++Register RExpr as gappa.gappa_private.RExpr.
++Register reUnknown as gappa.gappa_private.reUnknown.
++Register reInteger as gappa.gappa_private.reInteger.
++Register reFloat2 as gappa.gappa_private.reFloat2.
++Register reFloat10 as gappa.gappa_private.reFloat10.
++Register reUnary as gappa.gappa_private.reUnary.
++Register reBinary as gappa.gappa_private.reBinary.
++Register reBpow2 as gappa.gappa_private.reBpow2.
++Register reBpow10 as gappa.gappa_private.reBpow10.
++Register rePow2 as gappa.gappa_private.rePow2.
++Register rePow10 as gappa.gappa_private.rePow10.
++Register reRound as gappa.gappa_private.reRound.
++
+ Scheme Equality for positive.
+ Scheme Equality for Z.
+ Scheme Equality for UnaryOp.
+@@ -117,6 +150,14 @@ Inductive RAtom :=
+ | raGeneric : Format -> RExpr -> RAtom
+ | raFormat : Format -> RExpr -> RAtom.
+
++Register RAtom as gappa.gappa_private.RAtom.
++Register raBound as gappa.gappa_private.raBound.
++Register raRel as gappa.gappa_private.raRel.
++Register raEq as gappa.gappa_private.raEq.
++Register raLe as gappa.gappa_private.raLe.
++Register raGeneric as gappa.gappa_private.raGeneric.
++Register raFormat as gappa.gappa_private.raFormat.
++
+ Inductive RTree :=
+ | rtTrue : RTree
+ | rtFalse : RTree
+@@ -126,6 +167,15 @@ Inductive RTree :=
+ | rtOr : RTree -> RTree -> RTree
+ | rtImpl : RTree -> RTree -> RTree.
+
++Register RTree as gappa.gappa_private.RTree.
++Register rtTrue as gappa.gappa_private.rtTrue.
++Register rtFalse as gappa.gappa_private.rtFalse.
++Register rtAtom as gappa.gappa_private.rtAtom.
++Register rtNot as gappa.gappa_private.rtNot.
++Register rtAnd as gappa.gappa_private.rtAnd.
++Register rtOr as gappa.gappa_private.rtOr.
++Register rtImpl as gappa.gappa_private.rtImpl.
++
+ Section Convert.
+
+ Definition convert_exp (f : Format) : Z -> Z :=
+@@ -216,6 +266,8 @@ Fixpoint convert_tree (t : RTree) : Prop
+ | rtImpl t1 t2 => (convert_tree t1) -> (convert_tree t2)
+ end.
+
++Register convert_tree as gappa.gappa_private.convert_tree.
++
+ Lemma decidable_atom :
+ forall a, { convert_atom a } + { not (convert_atom a) }.
+ Proof with auto with typeclass_instances.
+@@ -1136,7 +1188,7 @@ Definition trans :=
+ trLeaf change_format_func change_format_prop ::
+ trLeaf remove_unknown_func remove_unknown_prop ::
+ trTree simplify_tree simplify_tree_correct ::
+- nil.
++ List.nil.
+
+ Theorem prepare_goal :
+ forall uv t,
+@@ -1181,4 +1233,7 @@ Ltac gappa_prepare :=
+ convert_apply ltac:(fun uv g => refine (prepare_goal uv g _)) ;
+ convert_apply ltac:(fun uv g => let g := eval vm_compute in g in change
(convert_tree uv g)).
+
++Require Rregisternames.
++Require Flocq.Core.Registernames.
++
+ Ltac gappa := abstract (gappa_prepare ; gappa_internal).
diff --git a/gappalib-coq.spec b/gappalib-coq.spec
index 96fb02e..1b9ec1b 100644
--- a/gappalib-coq.spec
+++ b/gappalib-coq.spec
@@ -7,16 +7,19 @@
# install the package and run "remake check" manually before committing.
%global gappadir %{_libdir}/coq/user-contrib/Gappa
-%global coqver 8.9.1
+%global coqver 8.11.0
Name: gappalib-coq
Version: 1.4.2
-Release: 5%{?dist}
+Release: 6%{?dist}
Summary: Coq support library for gappa
License: LGPLv2+
URL:
http://gappa.gforge.inria.fr/
Source0:
https://gforge.inria.fr/frs/download.php/file/38102/%{name}-%{version}.ta...
+# Adapt to coq 8.11.0
+#
https://github.com/MSoegtropIMC/gappa-coq/commit/d6f5177181c35f07ff50bd5c...
+Patch0: %{name}-coq811.patch
BuildRequires: gcc-c++
BuildRequires: coq = %{coqver}
@@ -50,7 +53,7 @@ files are not needed to use gappalib-coq. They are made available for
informational purposes.
%prep
-%setup -q
+%autosetup -p1
# Enable debuginfo
sed -i 's/-pp/-g &/' Remakefile.in
@@ -91,6 +94,9 @@ remake check
%{gappadir}/*.v
%changelog
+* Mon Mar 30 2020 Jerry James <loganjerry(a)gmail.com> - 1.4.2-6
+- Add -coq811 patch to fix the build with coq 8.11
+
* Tue Jan 28 2020 Fedora Release Engineering <releng(a)fedoraproject.org> - 1.4.2-5
- Rebuilt for
https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild