coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Yozo TODA
recent bulk builds show that coq 8.12.0 failed to build on
non ocaml-native architectures such as aarch64, sparc64, misp64.

by simulating non ocaml-native architectures on amd64
with arch-defines.mk modified,
(removing amd64 from OCAML_NATIVE_ARCHS and OCAML_DYNLINK_ARCHS)
I check how we should update PLIST and PFRAGs.

Here attached is the diff to coq-8.12.0.
Anyone please confirm this diff really enables the packaging
on non ocaml-native architectures?

-- yozo.

diff -ur coq-cur/Makefile coq-new/Makefile
--- coq-cur/Makefile Sun Aug  9 13:17:30 2020
+++ coq-new/Makefile Fri Aug 28 03:29:36 2020
@@ -3,6 +3,7 @@
 COMMENT= proof assistant based on a typed lambda calculus
 
 V= 8.12.0
+REVISION= 0
 GH_ACCOUNT = coq
 GH_PROJECT = coq
 GH_TAGNAME = V${V}
@@ -48,6 +49,7 @@
 ALL_TARGET= byte coq documentation \
  bin/coqide coqide-files theories/Init/Prelude.vo
 INSTALL_TARGET= install-coq install-byte install-meta
+RUN_DEPENDS+= math/ocaml-num
 .endif
 
 TEST_ENV= VERBOSE=1
diff -ur coq-cur/pkg/PFRAG.native coq-new/pkg/PFRAG.native
--- coq-cur/pkg/PFRAG.native Sun Aug  9 13:17:30 2020
+++ coq-new/pkg/PFRAG.native Fri Aug 28 04:05:52 2020
@@ -1,10 +1,23 @@
 @comment $OpenBSD: PFRAG.native,v 1.8 2020/08/09 02:45:35 daniel Exp $
 %%dynlink%%
+@bin bin/coq-tex
+@bin bin/coq_makefile
+@bin bin/coqc
+@bin bin/coqchk
+@bin bin/coqdep
+@bin bin/coqdoc
+@bin bin/coqide
+@bin bin/coqidetop
 @bin bin/coqidetop.opt
 @bin bin/coqproofworker.opt
 @bin bin/coqqueryworker.opt
 @bin bin/coqtacticworker.opt
 @bin bin/coqtop.opt
+@bin bin/coqtop
+@bin bin/coqwc
+@bin bin/coqworkmgr
+@bin bin/ocamllibdep
+@bin bin/votour
 lib/ocaml/coq/clib/bigint.cmx
 lib/ocaml/coq/clib/cArray.cmx
 lib/ocaml/coq/clib/cEphemeron.cmx
@@ -92,6 +105,7 @@
 lib/ocaml/coq/interp/smartlocate.cmx
 lib/ocaml/coq/interp/stdarg.cmx
 lib/ocaml/coq/interp/syntax_def.cmx
+@static-lib lib/ocaml/coq/kernel/byterun/libcoqrun.a
 lib/ocaml/coq/kernel/cClosure.cmx
 lib/ocaml/coq/kernel/cPrimitives.cmx
 lib/ocaml/coq/kernel/cbytecodes.cmx
@@ -283,6 +297,7 @@
 lib/ocaml/coq/plugins/ltac/tauto_plugin.o
 lib/ocaml/coq/plugins/micromega/certificate.cmx
 lib/ocaml/coq/plugins/micromega/coq_micromega.cmx
+@bin lib/ocaml/coq/plugins/micromega/csdpcert
 lib/ocaml/coq/plugins/micromega/csdpcert.cmx
 lib/ocaml/coq/plugins/micromega/g_micromega.cmx
 lib/ocaml/coq/plugins/micromega/g_zify.cmx
@@ -1695,3 +1710,4 @@
 lib/ocaml/coq/vernac/vernacinterp.cmx
 lib/ocaml/coq/vernac/vernacprop.cmx
 lib/ocaml/coq/vernac/vernacstate.cmx
+@man man/man1/coqtop.opt.1
diff -ur coq-cur/pkg/PFRAG.no-native coq-new/pkg/PFRAG.no-native
--- coq-cur/pkg/PFRAG.no-native Sat Jun  6 11:56:40 2020
+++ coq-new/pkg/PFRAG.no-native Fri Aug 28 04:01:49 2020
@@ -1,7 +1,27 @@
 @comment $OpenBSD: PFRAG.no-native,v 1.3 2020/06/01 06:04:50 chrisz Exp $
+bin/coq-tex
+bin/coq_makefile
+bin/coqc
+bin/coqchk
+bin/coqdep
+bin/coqdoc
+bin/coqide
+bin/coqidetop
+bin/coqidetop.byte
+bin/coqproofworker.byte
+bin/coqqueryworker.byte
+bin/coqtacticworker.byte
+bin/coqtop
+bin/coqtop.byte
+bin/coqwc
+bin/coqworkmgr
+bin/ocamllibdep
+bin/votour
 lib/ocaml/coq/clib/clib.cma
 lib/ocaml/coq/config/config.cma
+lib/ocaml/coq/dev/
 lib/ocaml/coq/dev/top_printers.cmi
+@so lib/ocaml/coq/dllcoqrun.so
 lib/ocaml/coq/engine/engine.cma
 lib/ocaml/coq/gramlib/.pack/gramlib.cma
 lib/ocaml/coq/ide/ide.cma
@@ -10,113 +30,24 @@
 lib/ocaml/coq/lib/lib.cma
 lib/ocaml/coq/library/library.cma
 lib/ocaml/coq/parsing/parsing.cma
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmo
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmo
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmo
 lib/ocaml/coq/plugins/btauto/btauto_plugin.cmo
 lib/ocaml/coq/plugins/cc/cc_plugin.cmo
-lib/ocaml/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmo
 lib/ocaml/coq/plugins/derive/derive_plugin.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmo
-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_ExtrOCamlFloats.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
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmo
-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/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
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Refl.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RingMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmo
+lib/ocaml/coq/plugins/micromega/csdpcert
 lib/ocaml/coq/plugins/micromega/micromega_plugin.cmo
 lib/ocaml/coq/plugins/micromega/zify_plugin.cmo
-lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
 lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmo
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmo
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaLemmas.cmo
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaPlugin.cmo
-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/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
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmo
 lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmo
 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/ssrsearch/ssrsearch_plugin.cmo
 lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmo
 lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmo
 lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmo
@@ -151,6 +82,7 @@
 lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Wf_nat.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.cmo
+lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_DecBool.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_IfProp.cmo
@@ -174,7 +106,7 @@
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmo
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmo
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.cmo
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmo
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.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
@@ -206,10 +138,13 @@
 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_Hexadecimal.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.cmo
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.cmo
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Prelude.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmo
@@ -290,8 +225,16 @@
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmo
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmo
@@ -394,13 +337,8 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ArithProp.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmo
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalConstructiveReals.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_DiscrR.cmo
@@ -452,6 +390,7 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_alt.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_calc.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmo
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.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
@@ -460,6 +399,18 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitRmult.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.cmo
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.cmo
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Definitions.cmo
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Operators.cmo
@@ -487,6 +438,7 @@
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3.cmo
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3_facts.cmo
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Uniset.cmo
+lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_CPermutation.cmo
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmo
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Mergesort.cmo
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_PermutEq.cmo
@@ -562,6 +514,121 @@
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmo
 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/theories/btauto/.coq-native/NCoq_btauto_Algebra.cmo
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.cmo
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.cmo
+lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.cmo
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.cmo
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.cmo
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.cmo
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.cmo
+lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo
+lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.cmo
 lib/ocaml/coq/toplevel/toplevel.cma
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmo
 lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmo
 lib/ocaml/coq/vernac/vernac.cma
+@man man/man1/coqtop.byte.1
diff -ur coq-cur/pkg/PLIST coq-new/pkg/PLIST
--- coq-cur/pkg/PLIST Sun Aug  9 13:17:31 2020
+++ coq-new/pkg/PLIST Fri Aug 28 04:14:14 2020
@@ -1,25 +1,7 @@
 @comment $OpenBSD: PLIST,v 1.16 2020/08/09 02:45:35 daniel Exp $
 %%native%%
 !%%native%%
-@bin bin/coq-tex
-@bin bin/coq_makefile
-@bin bin/coqc
-@bin bin/coqchk
-@bin bin/coqdep
-@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
-@bin bin/coqworkmgr
-@bin bin/ocamllibdep
-@bin bin/votour
 lib/ocaml/coq/
 lib/ocaml/coq/META
 lib/ocaml/coq/clib/
@@ -62,8 +44,6 @@
 lib/ocaml/coq/coqpp/coqpp_ast.cmi
 lib/ocaml/coq/coqpp/coqpp_parse.cmi
 lib/ocaml/coq/coqpp/coqpp_parser.cmi
-lib/ocaml/coq/dev/
-@comment lib/ocaml/coq/dllcoqrun.so
 lib/ocaml/coq/engine/
 lib/ocaml/coq/engine/eConstr.cmi
 lib/ocaml/coq/engine/evar_kinds.cmi
@@ -146,7 +126,6 @@
 lib/ocaml/coq/kernel/
 lib/ocaml/coq/kernel/byterun/
 @so lib/ocaml/coq/kernel/byterun/dllcoqrun.so
-@comment lib/ocaml/coq/kernel/byterun/libcoqrun.a
 lib/ocaml/coq/kernel/cClosure.cmi
 lib/ocaml/coq/kernel/cPrimitives.cmi
 lib/ocaml/coq/kernel/cbytecodes.cmi
@@ -320,7 +299,6 @@
 lib/ocaml/coq/plugins/micromega/
 lib/ocaml/coq/plugins/micromega/certificate.cmi
 lib/ocaml/coq/plugins/micromega/coq_micromega.cmi
-@bin lib/ocaml/coq/plugins/micromega/csdpcert
 lib/ocaml/coq/plugins/micromega/csdpcert.cmi
 lib/ocaml/coq/plugins/micromega/g_micromega.cmi
 lib/ocaml/coq/plugins/micromega/itv.cmi
@@ -3540,8 +3518,6 @@
 @man man/man1/coqdoc.1
 @man man/man1/coqide.1
 @man man/man1/coqtop.1
-@man man/man1/coqtop.byte.1
-@man man/man1/coqtop.opt.1
 @man man/man1/coqwc.1
 share/coq/
 share/coq/coq-ssreflect.lang
Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Charlene Wendling
On Fri, 28 Aug 2020 05:26:16 +0900
Yozo TODA wrote:

> recent bulk builds show that coq 8.12.0 failed to build on
> non ocaml-native architectures such as aarch64, sparc64, misp64.
>
> by simulating non ocaml-native architectures on amd64
> with arch-defines.mk modified,
> (removing amd64 from OCAML_NATIVE_ARCHS and OCAML_DYNLINK_ARCHS)
> I check how we should update PLIST and PFRAGs.
>
> Here attached is the diff to coq-8.12.0.
> Anyone please confirm this diff really enables the packaging
> on non ocaml-native architectures?
>
> -- yozo.

Hi,

It packages fine on macppc: https://bin.charlenew.xyz/coq.log

Charlène.

Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Yozo TODA
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Charlene Wendling writes:
> On Fri, 28 Aug 2020 05:26:16 +0900
> Yozo TODA wrote:
>
> > recent bulk builds show that coq 8.12.0 failed to build on
> > non ocaml-native architectures such as aarch64, sparc64, misp64.
........
> > Here attached is the diff to coq-8.12.0.
> > Anyone please confirm this diff really enables the packaging
> > on non ocaml-native architectures?
> >
> > -- yozo.
>
> Hi,
>
> It packages fine on macppc: https://bin.charlenew.xyz/coq.log

thanks.  I believe it verifies that my patch(8.12.0p0) works on
non ocaml-native architectures, too.

please commit this to the ports tree, anyone?

 -- yozo.

-----BEGIN PGP SIGNATURE-----

iQJJBAEBCgAzFiEEP48DGKttLBTWuiCMx2ep6SZGbGQFAl9eSXQVHHlvem9AdjAw
Ny52YWlvLm5lLmpwAAoJEMdnqekmRmxkT4AQAMCKnAe5hS1kIBYFTZLoXO9B5vni
GMKMFlC5G+Xen+Gz1i5IJSh+sn45466uZ0sbk0Bq5mN2Wx50qFXRd+LW8Ca4OPEh
FmAvbdrmCFBDPbqsJHXQtV0uUK90pyzDfeEpZA9TCivHK/TwRgNt8fsRqeCe0hzF
38NiUa+XPVIIFRet9XfBOvGVltIvxW+zBQ4SHHUKgf/1puxi3FzuurV60glTpX6B
PZsJBPFLyHXw50vEg0jWHjqisRElL2BzhDq10fi8KBJo51F1OkW2goHYX4kdwJIB
Br1i/zy3SILDcnzSn85p/vxIv+phIT0jeR5KkL4rihSV2NC/D7Bk6/kFudEDlnyi
IStrgFQ3Qed0kfeCjQekxmJ7JiVG30DRP5vPLqtswLbCMkcDEOAj9IGfWflQi1X2
rwCTuXux/qP71ZYXoHu4tu5b6kAADNVeXwFQnYYrMcaHkOpEwkhfShtt4W8d2Y46
/5cJY8AYj/aCtAcP3OnlmgiZBM1YIbQZKSub8cleta3bFRc2PUV/iu0BT0GmKscx
/7TGN5i2S78Di2T/p2L5QAbim1ytQEaX0UUGpmeLLInD5eZyhAXqxZG2yjueIopJ
dD/bdbG45coh6AUmAqxsO4WeJbzKbjxK/k4vaJN1+GoHBVLQAPb7FHwStyW6flSv
Q2N9Ap7a6YyJvkG+
=3/PT
-----END PGP SIGNATURE-----

diff -ur coq-cur/Makefile coq-new/Makefile
--- coq-cur/Makefile Sun Aug  9 13:17:30 2020
+++ coq-new/Makefile Fri Aug 28 03:29:36 2020
@@ -3,6 +3,7 @@
 COMMENT= proof assistant based on a typed lambda calculus
 
 V= 8.12.0
+REVISION= 0
 GH_ACCOUNT = coq
 GH_PROJECT = coq
 GH_TAGNAME = V${V}
@@ -48,6 +49,7 @@
 ALL_TARGET= byte coq documentation \
  bin/coqide coqide-files theories/Init/Prelude.vo
 INSTALL_TARGET= install-coq install-byte install-meta
+RUN_DEPENDS+= math/ocaml-num
 .endif
 
 TEST_ENV= VERBOSE=1
diff -ur coq-cur/pkg/PFRAG.native coq-new/pkg/PFRAG.native
--- coq-cur/pkg/PFRAG.native Sun Aug  9 13:17:30 2020
+++ coq-new/pkg/PFRAG.native Fri Aug 28 04:05:52 2020
@@ -1,10 +1,23 @@
 @comment $OpenBSD: PFRAG.native,v 1.8 2020/08/09 02:45:35 daniel Exp $
 %%dynlink%%
+@bin bin/coq-tex
+@bin bin/coq_makefile
+@bin bin/coqc
+@bin bin/coqchk
+@bin bin/coqdep
+@bin bin/coqdoc
+@bin bin/coqide
+@bin bin/coqidetop
 @bin bin/coqidetop.opt
 @bin bin/coqproofworker.opt
 @bin bin/coqqueryworker.opt
 @bin bin/coqtacticworker.opt
 @bin bin/coqtop.opt
+@bin bin/coqtop
+@bin bin/coqwc
+@bin bin/coqworkmgr
+@bin bin/ocamllibdep
+@bin bin/votour
 lib/ocaml/coq/clib/bigint.cmx
 lib/ocaml/coq/clib/cArray.cmx
 lib/ocaml/coq/clib/cEphemeron.cmx
@@ -92,6 +105,7 @@
 lib/ocaml/coq/interp/smartlocate.cmx
 lib/ocaml/coq/interp/stdarg.cmx
 lib/ocaml/coq/interp/syntax_def.cmx
+@static-lib lib/ocaml/coq/kernel/byterun/libcoqrun.a
 lib/ocaml/coq/kernel/cClosure.cmx
 lib/ocaml/coq/kernel/cPrimitives.cmx
 lib/ocaml/coq/kernel/cbytecodes.cmx
@@ -283,6 +297,7 @@
 lib/ocaml/coq/plugins/ltac/tauto_plugin.o
 lib/ocaml/coq/plugins/micromega/certificate.cmx
 lib/ocaml/coq/plugins/micromega/coq_micromega.cmx
+@bin lib/ocaml/coq/plugins/micromega/csdpcert
 lib/ocaml/coq/plugins/micromega/csdpcert.cmx
 lib/ocaml/coq/plugins/micromega/g_micromega.cmx
 lib/ocaml/coq/plugins/micromega/g_zify.cmx
@@ -1695,3 +1710,4 @@
 lib/ocaml/coq/vernac/vernacinterp.cmx
 lib/ocaml/coq/vernac/vernacprop.cmx
 lib/ocaml/coq/vernac/vernacstate.cmx
+@man man/man1/coqtop.opt.1
diff -ur coq-cur/pkg/PFRAG.no-native coq-new/pkg/PFRAG.no-native
--- coq-cur/pkg/PFRAG.no-native Sat Jun  6 11:56:40 2020
+++ coq-new/pkg/PFRAG.no-native Fri Aug 28 04:01:49 2020
@@ -1,7 +1,27 @@
 @comment $OpenBSD: PFRAG.no-native,v 1.3 2020/06/01 06:04:50 chrisz Exp $
+bin/coq-tex
+bin/coq_makefile
+bin/coqc
+bin/coqchk
+bin/coqdep
+bin/coqdoc
+bin/coqide
+bin/coqidetop
+bin/coqidetop.byte
+bin/coqproofworker.byte
+bin/coqqueryworker.byte
+bin/coqtacticworker.byte
+bin/coqtop
+bin/coqtop.byte
+bin/coqwc
+bin/coqworkmgr
+bin/ocamllibdep
+bin/votour
 lib/ocaml/coq/clib/clib.cma
 lib/ocaml/coq/config/config.cma
+lib/ocaml/coq/dev/
 lib/ocaml/coq/dev/top_printers.cmi
+@so lib/ocaml/coq/dllcoqrun.so
 lib/ocaml/coq/engine/engine.cma
 lib/ocaml/coq/gramlib/.pack/gramlib.cma
 lib/ocaml/coq/ide/ide.cma
@@ -10,113 +30,24 @@
 lib/ocaml/coq/lib/lib.cma
 lib/ocaml/coq/library/library.cma
 lib/ocaml/coq/parsing/parsing.cma
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmo
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmo
-lib/ocaml/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmo
 lib/ocaml/coq/plugins/btauto/btauto_plugin.cmo
 lib/ocaml/coq/plugins/cc/cc_plugin.cmo
-lib/ocaml/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmo
 lib/ocaml/coq/plugins/derive/derive_plugin.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmo
-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_ExtrOCamlFloats.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
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmo
-lib/ocaml/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmo
-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/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
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Refl.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_RingMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Tauto.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_VarMap.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZCoeff.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZMicromega.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Zify.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyBool.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyInst.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_ZifyPow.cmo
-lib/ocaml/coq/plugins/micromega/.coq-native/NCoq_micromega_Ztac.cmo
+lib/ocaml/coq/plugins/micromega/csdpcert
 lib/ocaml/coq/plugins/micromega/micromega_plugin.cmo
 lib/ocaml/coq/plugins/micromega/zify_plugin.cmo
-lib/ocaml/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
 lib/ocaml/coq/plugins/nsatz/nsatz_plugin.cmo
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmo
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaLemmas.cmo
-lib/ocaml/coq/plugins/omega/.coq-native/NCoq_omega_OmegaPlugin.cmo
-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/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
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmo
-lib/ocaml/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmo
 lib/ocaml/coq/plugins/setoid_ring/newring_plugin.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrclasses.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmo
-lib/ocaml/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrunder.cmo
 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/ssrsearch/ssrsearch_plugin.cmo
 lib/ocaml/coq/plugins/syntax/float_syntax_plugin.cmo
 lib/ocaml/coq/plugins/syntax/int63_syntax_plugin.cmo
 lib/ocaml/coq/plugins/syntax/numeral_notation_plugin.cmo
@@ -151,6 +82,7 @@
 lib/ocaml/coq/theories/Arith/.coq-native/NCoq_Arith_Wf_nat.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bool.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolEq.cmo
+lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_BoolOrder.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_Bvector.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_DecBool.cmo
 lib/ocaml/coq/theories/Bool/.coq-native/NCoq_Bool_IfProp.cmo
@@ -174,7 +106,7 @@
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmo
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq810.cmo
 lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq811.cmo
-lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq89.cmo
+lib/ocaml/coq/theories/Compat/.coq-native/NCoq_Compat_Coq812.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
@@ -206,10 +138,13 @@
 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_Hexadecimal.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Logic_Type.cmo
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Ltac.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Nat.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Notations.cmo
+lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Numeral.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Peano.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Prelude.cmo
 lib/ocaml/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmo
@@ -290,8 +225,16 @@
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalN.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalNat.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalPos.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalQ.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalString.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_DecimalZ.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalFacts.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalN.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalNat.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalPos.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalQ.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalString.cmo
+lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_HexadecimalZ.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NaryFunctions.cmo
 lib/ocaml/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmo
 lib/ocaml/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmo
@@ -394,13 +337,8 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ArithProp.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Binomial.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cauchy_prod.cmo
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalConstructiveReals.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ClassicalDedekindReals.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyReals.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveCauchyRealsMult.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRcomplete.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveReals.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsLUB.cmo
-lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_ConstructiveRealsMorphisms.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_plus.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Cos_rel.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_DiscrR.cmo
@@ -452,6 +390,7 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_alt.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_calc.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_def.cmo
+lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Rtrigo_facts.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
@@ -460,6 +399,18 @@
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitAbsolu.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_SplitRmult.cmo
 lib/ocaml/coq/theories/Reals/.coq-native/NCoq_Reals_Sqrt_reg.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveAbs.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLUB.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveLimits.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveMinMax.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructivePower.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveReals.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cmo
+lib/ocaml/coq/theories/Reals/Abstract/.coq-native/NCoq_Reals_Abstract_ConstructiveSum.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cmo
+lib/ocaml/coq/theories/Reals/Cauchy/.coq-native/NCoq_Reals_Cauchy_ConstructiveRcomplete.cmo
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Operators_Properties.cmo
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Definitions.cmo
 lib/ocaml/coq/theories/Relations/.coq-native/NCoq_Relations_Relation_Operators.cmo
@@ -487,6 +438,7 @@
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3.cmo
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Relations_3_facts.cmo
 lib/ocaml/coq/theories/Sets/.coq-native/NCoq_Sets_Uniset.cmo
+lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_CPermutation.cmo
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Heap.cmo
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_Mergesort.cmo
 lib/ocaml/coq/theories/Sorting/.coq-native/NCoq_Sorting_PermutEq.cmo
@@ -562,6 +514,121 @@
 lib/ocaml/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmo
 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/theories/btauto/.coq-native/NCoq_btauto_Algebra.cmo
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Btauto.cmo
+lib/ocaml/coq/theories/btauto/.coq-native/NCoq_btauto_Reflect.cmo
+lib/ocaml/coq/theories/derive/.coq-native/NCoq_derive_Derive.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlFloats.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlNativeString.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmo
+lib/ocaml/coq/theories/extraction/.coq-native/NCoq_extraction_Extraction.cmo
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_FunInd.cmo
+lib/ocaml/coq/theories/funind/.coq-native/NCoq_funind_Recdef.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_DeclConstant.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Env.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_EnvRing.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Fourier_util.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lia.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lqa.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Lra.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_MExtraction.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Psatz.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_QMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Refl.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_RingMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Tauto.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_VarMap.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZArith_hints.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZCoeff.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZMicromega.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Zify.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyBool.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyClasses.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyComparison.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyInst.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_ZifyPow.cmo
+lib/ocaml/coq/theories/micromega/.coq-native/NCoq_micromega_Ztac.cmo
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
+lib/ocaml/coq/theories/nsatz/.coq-native/NCoq_nsatz_NsatzTactic.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_Omega.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaLemmas.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaPlugin.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_OmegaTactic.cmo
+lib/ocaml/coq/theories/omega/.coq-native/NCoq_omega_PreOmega.cmo
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo
+lib/ocaml/coq/theories/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_BinList.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Cring.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_tac.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Field_theory.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_InitialRing.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Integral_domain.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_NArithRing.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_initial.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_polynom.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ncring_tac.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_RealField.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_base.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_polynom.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_tac.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Ring_theory.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Q.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_R.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_Rings_Z.cmo
+lib/ocaml/coq/theories/setoid_ring/.coq-native/NCoq_setoid_ring_ZArithRing.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrbool.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrclasses.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssreflect.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrfun.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrsetoid.cmo
+lib/ocaml/coq/theories/ssr/.coq-native/NCoq_ssr_ssrunder.cmo
+lib/ocaml/coq/theories/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo
+lib/ocaml/coq/theories/ssrsearch/.coq-native/NCoq_ssrsearch_ssrsearch.cmo
 lib/ocaml/coq/toplevel/toplevel.cma
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Array.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Bool.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Char.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Constr.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Control.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Env.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Fresh.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ident.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Init.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Int.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_List.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac1.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ltac2.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Message.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Notations.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Option.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pattern.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_Std.cmo
+lib/ocaml/coq/user-contrib/Ltac2/.coq-native/NLtac2_String.cmo
 lib/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmo
 lib/ocaml/coq/vernac/vernac.cma
+@man man/man1/coqtop.byte.1
diff -ur coq-cur/pkg/PLIST coq-new/pkg/PLIST
--- coq-cur/pkg/PLIST Sun Aug  9 13:17:31 2020
+++ coq-new/pkg/PLIST Fri Aug 28 04:14:14 2020
@@ -1,25 +1,7 @@
 @comment $OpenBSD: PLIST,v 1.16 2020/08/09 02:45:35 daniel Exp $
 %%native%%
 !%%native%%
-@bin bin/coq-tex
-@bin bin/coq_makefile
-@bin bin/coqc
-@bin bin/coqchk
-@bin bin/coqdep
-@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
-@bin bin/coqworkmgr
-@bin bin/ocamllibdep
-@bin bin/votour
 lib/ocaml/coq/
 lib/ocaml/coq/META
 lib/ocaml/coq/clib/
@@ -62,8 +44,6 @@
 lib/ocaml/coq/coqpp/coqpp_ast.cmi
 lib/ocaml/coq/coqpp/coqpp_parse.cmi
 lib/ocaml/coq/coqpp/coqpp_parser.cmi
-lib/ocaml/coq/dev/
-@comment lib/ocaml/coq/dllcoqrun.so
 lib/ocaml/coq/engine/
 lib/ocaml/coq/engine/eConstr.cmi
 lib/ocaml/coq/engine/evar_kinds.cmi
@@ -146,7 +126,6 @@
 lib/ocaml/coq/kernel/
 lib/ocaml/coq/kernel/byterun/
 @so lib/ocaml/coq/kernel/byterun/dllcoqrun.so
-@comment lib/ocaml/coq/kernel/byterun/libcoqrun.a
 lib/ocaml/coq/kernel/cClosure.cmi
 lib/ocaml/coq/kernel/cPrimitives.cmi
 lib/ocaml/coq/kernel/cbytecodes.cmi
@@ -320,7 +299,6 @@
 lib/ocaml/coq/plugins/micromega/
 lib/ocaml/coq/plugins/micromega/certificate.cmi
 lib/ocaml/coq/plugins/micromega/coq_micromega.cmi
-@bin lib/ocaml/coq/plugins/micromega/csdpcert
 lib/ocaml/coq/plugins/micromega/csdpcert.cmi
 lib/ocaml/coq/plugins/micromega/g_micromega.cmi
 lib/ocaml/coq/plugins/micromega/itv.cmi
@@ -3540,8 +3518,6 @@
 @man man/man1/coqdoc.1
 @man man/man1/coqide.1
 @man man/man1/coqtop.1
-@man man/man1/coqtop.byte.1
-@man man/man1/coqtop.opt.1
 @man man/man1/coqwc.1
 share/coq/
 share/coq/coq-ssreflect.lang
Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Daniel Dickman


On Mon, 14 Sep 2020, Yozo TODA wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA512
>
> Charlene Wendling writes:
> > On Fri, 28 Aug 2020 05:26:16 +0900
> > Yozo TODA wrote:
> >
> > > recent bulk builds show that coq 8.12.0 failed to build on
> > > non ocaml-native architectures such as aarch64, sparc64, misp64.
> ........
> > > Here attached is the diff to coq-8.12.0.
> > > Anyone please confirm this diff really enables the packaging
> > > on non ocaml-native architectures?
> > >
> > > -- yozo.
> >
> > Hi,
> >
> > It packages fine on macppc: https://bin.charlenew.xyz/coq.log
>
> thanks.  I believe it verifies that my patch(8.12.0p0) works on
> non ocaml-native architectures, too.
>
> please commit this to the ports tree, anyone?
>

We now include coqc in both PFRAG.no-native and PFRAG.native which seems a
bit unusual to me.

Are you sure this change is correct?

Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Yozo TODA
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

> We now include coqc in both PFRAG.no-native and PFRAG.native which seems a
> bit unusual to me.
>
> Are you sure this change is correct?

ah sorry, I should add more explanation.

  - adding ocaml-num in RUN_DEPENDS for non ocaml_native architectures

    when I tried packaging on amd64 (with arch-defines.mk modified),
    I found coqtop requires ocaml-num.
    with ocaml-num installed coqtop works.
    (I didn't note which file at that time, but I believe
     what is required is dllnums.so)

    for ocaml_native architectures, we don't need ocaml-num for RUN_DEPENDS.
    (I didn't check further, maybe ocaml-num is compiled in?)


  - some files in both PFRAG.no-native and PFRAG.native

    some files are native binaries on ocaml_native architectures (marked @bin),
    whereas byte-compiled on non ocaml_native architectures.

    My patch put those files to both PFRAG.native and PFRAG.no-native,
    but I think we can put those to PLIST.
    Which is better?  (how is @bin marking important?)

    $ for i in  \
          `cat /usr/ports/mystuff/math/coq/pkg/P* | awk '{print $NF;}' | sort |  uniq -c |\
           egrep -v  '^ *1' | tail -n +2 | awk '{print $NF;}'`;
      do
        ( grep $i /usr/ports/mystuff/math/coq/pkg/P* );
      done | head -10
    /usr/ports/mystuff/math/coq/pkg/PFRAG.native:@bin bin/coq-tex
    /usr/ports/mystuff/math/coq/pkg/PFRAG.no-native:bin/coq-tex
    /usr/ports/mystuff/math/coq/pkg/PFRAG.native:@bin bin/coq_makefile
    /usr/ports/mystuff/math/coq/pkg/PFRAG.no-native:bin/coq_makefile
    /usr/ports/mystuff/math/coq/pkg/PFRAG.native:@bin bin/coqc
    /usr/ports/mystuff/math/coq/pkg/PFRAG.native:@bin bin/coqchk
    /usr/ports/mystuff/math/coq/pkg/PFRAG.native:lib/ocaml/coq/topbin/coqc_bin.cmx
    /usr/ports/mystuff/math/coq/pkg/PFRAG.no-native:bin/coqc
    /usr/ports/mystuff/math/coq/pkg/PFRAG.no-native:bin/coqchk
    /usr/ports/mystuff/math/coq/pkg/PFRAG.native:@bin bin/coqchk
    $

 -- yozo.

-----BEGIN PGP SIGNATURE-----

iQJJBAEBCgAzFiEEP48DGKttLBTWuiCMx2ep6SZGbGQFAl9gDWAVHHlvem9AdjAw
Ny52YWlvLm5lLmpwAAoJEMdnqekmRmxk+OoP/0vi1P3LOoVijc8O5GP/QgpLi5uc
YfCA0nEewY0gI/opauom/e1oH9mgD4RVeg/jHv6nBXDI1oTGIkOc+PUuQ8SOgcBH
kTKX3Np5lhq5ScNeUU0zoLNEOyoucv2b8e0UOM8k5IWY04vHq1byVfvAASd1Zm0E
xH+GvZm4QcntPQPV5vI1Hek1CC35PJ7eYoCdMLILpvMy0ZAoGnxMFw2DEe05+W5P
/0N7X+PnDpNguLMsH+zkYcqfM/W+1kbfiZgv/dVKNogaA7vkQl5mM5ob0Mh1Rtbh
F4yecVa0/bjehFN6yBMaLfjcRFpQCvaAPC5EhVLPS5yY2XpMLbRyuUf3nXSgcwhT
7xgxVUHYMQXpRmtJZYeV96WFWr6IWYLeQqwNjYKfWw3Qg2VNn60lQn+Eykq1VzZu
3PrJTu94216LHUUuaK1Tj9/gZb/5NwHiPVkRIRaj52pYgzRj3JetO053cKGZVk3q
LYT5ZvElhkest3R72lvD/ObQEq27S4qnvDkuRja6FegkgXSCWaZe2Y8z62/J8ePR
22FSa230CrAcNqy+PHWwb2mBv7LpIJutboCfMOFtTpgmRu5nVpBel78y+2uOdFwm
2JzFsZ7Wvdd2qAYdCDVRsl4IUHmMMkKMwA6/a8ztAyqAgeGIyiR1UL9KF0v7eYx+
ruaKgks0C+I8Bs7u
=HlC7
-----END PGP SIGNATURE-----

Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Janne Johansson-3
In reply to this post by Charlene Wendling
Seems to build and install ok on mips64 too:

http://c66.it.su.se:8080/obsd/coq-build-mips64.txt

Don't know how to test it further than that.


Den sön 30 aug. 2020 kl 19:57 skrev Charlene Wendling <[hidden email]
>:

> On Fri, 28 Aug 2020 05:26:16 +0900
> Yozo TODA wrote:
>
> > recent bulk builds show that coq 8.12.0 failed to build on
> > non ocaml-native architectures such as aarch64, sparc64, misp64.
> >
> > by simulating non ocaml-native architectures on amd64
> > with arch-defines.mk modified,
> > (removing amd64 from OCAML_NATIVE_ARCHS and OCAML_DYNLINK_ARCHS)
> > I check how we should update PLIST and PFRAGs.
> >
> > Here attached is the diff to coq-8.12.0.
> > Anyone please confirm this diff really enables the packaging
> > on non ocaml-native architectures?
> >
> > -- yozo.
>
> Hi,
>
> It packages fine on macppc: https://bin.charlenew.xyz/coq.log
>
> Charlène.
>
>

--
May the most significant bit of your life be positive.
Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Daniel Dickman
In reply to this post by Yozo TODA

> On Sep 14, 2020, at 8:43 PM, Yozo TODA <[hidden email]> wrote:
>
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA512
>
>> We now include coqc in both PFRAG.no-native and PFRAG.native which seems a
>> bit unusual to me.
>>
>> Are you sure this change is correct?
>
> ah sorry, I should add more explanation.

Thanks!

I’ve committed your diff except for the PLIST changes.

Took me a few days as I wanted to confirm it all on powerpc and my powerpc box is not fast.

Hopefully this will now fix both the packaging problem and the core dumps seen in recent !native bulk builds...

Reply | Threaded
Open this post in threaded view
|

Re: coq 8.12.0p0: diff to unbreak on non-ocaml-native architecture

Daniel Dickman
In reply to this post by Janne Johansson-3

> On Sep 16, 2020, at 2:22 AM, Janne Johansson <[hidden email]> wrote:
>
> Seems to build and install ok on mips64 too:
>
> http://c66.it.su.se:8080/obsd/coq-build-mips64.txt
>
> Don't know how to test it further than that.
>

Thanks!

“make test” would be one way to check coq runtime functionality. Although it may take hours to complete if you let it run the whole way through....