Hi,
for building bytecode-only coq I need the following patch. (Did I send
you this before? I misconfigured my mail client.) OK?
Christopher
Index: Makefile
===================================================================
RCS file: /cvs/ports/math/coq/Makefile,v
retrieving revision 1.45
diff -u -p -r1.45 Makefile
--- Makefile 27 Sep 2019 09:58:09 -0000 1.45
+++ Makefile 28 Sep 2019 18:39:38 -0000
@@ -3,6 +3,7 @@
COMMENT= proof assistant based on a typed lambda calculus
V= 8.10+beta3
+REVISION = 0
GH_ACCOUNT = coq
GH_PROJECT = coq
GH_TAGNAME = V${V}
Index: pkg/PFRAG.native
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PFRAG.native,v
retrieving revision 1.5
diff -u -p -r1.5 PFRAG.native
--- pkg/PFRAG.native 20 Sep 2019 03:28:34 -0000 1.5
+++ pkg/PFRAG.native 28 Sep 2019 18:39:38 -0000
@@ -578,6 +578,7 @@ lib/ocaml/coq/proofs/refine.cmx
lib/ocaml/coq/proofs/refiner.cmx
lib/ocaml/coq/proofs/tacmach.cmx
lib/ocaml/coq/proofs/tactypes.cmx
+lib/ocaml/coq/revision
lib/ocaml/coq/stm/asyncTaskQueue.cmx
lib/ocaml/coq/stm/coqworkmgrApi.cmx
lib/ocaml/coq/stm/dag.cmx
@@ -1461,6 +1462,7 @@ lib/ocaml/coq/theories/ZArith/.coq-nativ
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.o
+lib/ocaml/coq/topbin/
lib/ocaml/coq/topbin/coqc_bin.cmx
lib/ocaml/coq/topbin/coqproofworker_bin.cmx
lib/ocaml/coq/topbin/coqqueryworker_bin.cmx
Index: pkg/PFRAG.no-native
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PFRAG.no-native,v
retrieving revision 1.1
diff -u -p -r1.1 PFRAG.no-native
--- pkg/PFRAG.no-native 4 Mar 2019 12:51:15 -0000 1.1
+++ pkg/PFRAG.no-native 28 Sep 2019 18:39:38 -0000
@@ -1,10 +1,11 @@
@comment $OpenBSD: PFRAG.no-native,v 1.1 2019/03/04 12:51:15 chrisz Exp $
lib/ocaml/coq/clib/clib.cma
+lib/ocaml/coq/config/config.cma
lib/ocaml/coq/dev/top_printers.cmi
lib/ocaml/coq/engine/engine.cma
+lib/ocaml/coq/gramlib/.pack/gramlib.cma
lib/ocaml/coq/ide/ide.cma
lib/ocaml/coq/interp/interp.cma
-lib/ocaml/coq/intf/intf.cma
lib/ocaml/coq/kernel/kernel.cma
lib/ocaml/coq/lib/lib.cma
lib/ocaml/coq/library/library.cma
@@ -24,6 +25,7 @@ lib/ocaml/coq/plugins/extraction/.coq-na
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmo
+lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmo
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmo
@@ -35,17 +37,17 @@ lib/ocaml/coq/plugins/extraction/.coq-na
lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmo
lib/ocaml/coq/plugins/extraction/extraction_plugin.cmo
lib/ocaml/coq/plugins/firstorder/ground_plugin.cmo
-lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmo
-lib/ocaml/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmo
-lib/ocaml/coq/plugins/fourier/fourier_plugin.cmo
lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmo
lib/ocaml/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmo
lib/ocaml/coq/plugins/funind/recdef_plugin.cmo
lib/ocaml/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmo
lib/ocaml/coq/plugins/ltac/ltac_plugin.cmo
lib/ocaml/coq/plugins/ltac/tauto_plugin.cmo
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_DeclConstant.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmo
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier.cmo
+lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Fourier_util.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmo
lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmo
@@ -69,11 +71,6 @@ lib/ocaml/coq/plugins/omega/.coq-native/
lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaTactic.cmo
lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_PreOmega.cmo
lib/ocaml/coq/plugins/omega/omega_plugin.cmo
-lib/ocaml/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmo
-lib/ocaml/coq/plugins/quote/quote_plugin.cmo
-lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmo
-lib/ocaml/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmo
-lib/ocaml/coq/plugins/romega/romega_plugin.cmo
lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo
lib/ocaml/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmo
lib/ocaml/coq/plugins/rtauto/rtauto_plugin.cmo
@@ -108,12 +105,10 @@ lib/ocaml/coq/plugins/ssr/.coq-native/NC
lib/ocaml/coq/plugins/ssr/ssreflect_plugin.cmo
lib/ocaml/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo
lib/ocaml/coq/plugins/ssrmatching/ssrmatching_plugin.cmo
-lib/ocaml/coq/plugins/syntax/ascii_syntax_plugin.cmo
-lib/ocaml/coq/plugins/syntax/int31_syntax_plugin.cmo
-lib/ocaml/coq/plugins/syntax/nat_syntax_plugin.cmo
+lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmo
+lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmo
lib/ocaml/coq/plugins/syntax/r_syntax_plugin.cmo
-lib/ocaml/coq/plugins/syntax/string_syntax_plugin.cmo
-lib/ocaml/coq/plugins/syntax/z_syntax_plugin.cmo
+lib/ocaml/coq/plugins/syntax/string_notation_plugin.cmo
lib/ocaml/coq/pretyping/pretyping.cma
lib/ocaml/coq/printing/printing.cma
lib/ocaml/coq/proofs/proofs.cma
@@ -164,9 +159,9 @@ lib/ocaml/coq/theories/Classes/.coq-nati
lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidDec.cmo
lib/ocaml/coq/theories/Classes/.coq-native/NCoq_Classes_SetoidTactics.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmo
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmo
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq87.cmo
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmo
lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq88.cmo
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFullAVL.cmo
@@ -188,6 +183,7 @@ lib/ocaml/coq/theories/FSets/.coq-native
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetToFiniteSet.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSetWeakList.cmo
lib/ocaml/coq/theories/FSets/.coq-native/NCoq_FSets_FSets.cmo
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Byte.cmo
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Datatypes.cmo
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Decimal.cmo
lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmo
@@ -241,6 +237,7 @@ lib/ocaml/coq/theories/Logic/.coq-native
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmo
+lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_StrictProp.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmo
lib/ocaml/coq/theories/Logic/.coq-native/NCoq_Logic_WeakFan.cmo
lib/ocaml/coq/theories/MSets/.coq-native/NCoq_MSets_MSetAVL.cmo
@@ -266,6 +263,7 @@ lib/ocaml/coq/theories/NArith/.coq-nativ
lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Ngcd_def.cmo
lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nnat.cmo
lib/ocaml/coq/theories/NArith/.coq-native/NCoq_NArith_Nsqrt_def.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_AltBinNotations.cmo
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmo
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalFacts.cmo
lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmo
@@ -281,6 +279,9 @@ lib/ocaml/coq/theories/Numbers/Cyclic/Ab
lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmo
lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Int31.cmo
lib/ocaml/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Ring31.cmo
+lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Cyclic63.cmo
+lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Int63.cmo
+lib/ocaml/coq/theories/Numbers/Cyclic/Int63/.coq-native/NCoq_Numbers_Cyclic_Int63_Ring63.cmo
lib/ocaml/coq/theories/Numbers/Cyclic/ZModulo/.coq-native/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cmo
lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAdd.cmo
lib/ocaml/coq/theories/Numbers/Integer/Abstract/.coq-native/NCoq_Numbers_Integer_Abstract_ZAddOrder.cmo
@@ -424,6 +425,7 @@ lib/ocaml/coq/theories/Reals/.coq-native
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_fun.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_reg.cmo
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Runcountable.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqProp.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SeqSeries.cmo
lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmo
@@ -464,6 +466,11 @@ lib/ocaml/coq/theories/Sorting/.coq-nati
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorted.cmo
lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Sorting.cmo
lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Ascii.cmo
+lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmo
+lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmo
+lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmo
+lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmo
+lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmo
lib/ocaml/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmo
lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableType.cmo
lib/ocaml/coq/theories/Structures/.coq-native/NCoq_Structures_DecidableTypeEx.cmo
@@ -529,8 +536,4 @@ lib/ocaml/coq/theories/ZArith/.coq-nativ
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmo
lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmo
lib/ocaml/coq/toplevel/toplevel.cma
-lib/ocaml/coq/toploop/coqidetop.cma
-lib/ocaml/coq/toploop/queryworkertop.cma
-lib/ocaml/coq/toploop/proofworkertop.cma
-lib/ocaml/coq/toploop/tacworkertop.cma
lib/ocaml/coq/vernac/vernac.cma
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/math/coq/pkg/PLIST,v
retrieving revision 1.13
diff -u -p -r1.13 PLIST
--- pkg/PLIST 20 Sep 2019 03:28:34 -0000 1.13
+++ pkg/PLIST 28 Sep 2019 18:39:39 -0000
@@ -1,5 +1,6 @@
@comment $OpenBSD: PLIST,v 1.13 2019/09/20 03:28:34 daniel Exp $
%%native%%
+!%%native%%
@bin bin/coq-tex
@bin bin/coq_makefile
@bin bin/coqc
@@ -8,7 +9,11 @@
@bin bin/coqdoc
@bin bin/coqide
@bin bin/coqidetop
+@comment bin/coqidetop.byte
bin/coqpp
+@comment bin/coqproofworker.byte
+@comment bin/coqqueryworker.byte
+@comment bin/coqtacticworker.byte
@bin bin/coqtop
@comment bin/coqtop.byte
@bin bin/coqwc
@@ -767,7 +772,6 @@ lib/ocaml/coq/proofs/refine.cmi
lib/ocaml/coq/proofs/refiner.cmi
lib/ocaml/coq/proofs/tacmach.cmi
lib/ocaml/coq/proofs/tactypes.cmi
-lib/ocaml/coq/revision
lib/ocaml/coq/stm/
lib/ocaml/coq/stm/asyncTaskQueue.cmi
lib/ocaml/coq/stm/coqworkmgrApi.cmi
@@ -2576,7 +2580,6 @@ lib/ocaml/coq/tools/coqdoc/coqdoc.sty
lib/ocaml/coq/tools/make-both-single-timing-files.py
lib/ocaml/coq/tools/make-both-time-files.py
lib/ocaml/coq/tools/make-one-time-file.py
-lib/ocaml/coq/topbin/
lib/ocaml/coq/toplevel/
lib/ocaml/coq/toplevel/ccompile.cmi
lib/ocaml/coq/toplevel/coqargs.cmi
--
http://gmerlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1
