Hi, I'd rather commit this fix now so that there is a chance to build test it on different architectures in bulk-builds. OK?
Christopher -- http://gmerlin.de OpenPGP: http://gmerlin.de/christopher.pub CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1
? diff 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 6 Oct 2019 17:08:23 -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 6 Oct 2019 17:08:23 -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 6 Oct 2019 17:08:24 -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 6 Oct 2019 17:08:24 -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