>>> Building on exopi-6 under lang/compcert BDEPENDS = [lang/gcc/8;lang/gcc/8,-c++;lang/gcc/8,-libs;devel/ocaml-menhir;sysutils/findlib;devel/gmake;math/coq;lang/ocaml] DIST = [lang/compcert:CompCert-3.13.1.tar.gz] FULLPKGNAME = compcert-3.13.1p1 RDEPENDS = [lang/gcc/8,-libs;lang/gcc/8] (Junk lock obtained for exopi-6 at 1735045924.28) >>> Running depends in lang/compcert at 1735045924.32 last junk was in x11/kde-applications/kdepim-runtime /usr/sbin/pkg_add -aI -Drepair coq-8.13.2p6 findlib-1.9.6p2 g++-8.4.0p25 gcc-8.4.0p25 gcc-libs-8.4.0p25 gmake-4.4.1 ocaml-4.14.2 ocaml-menhir-20230608p1 was: /usr/sbin/pkg_add -aI -Drepair coq-8.13.2p6 findlib-1.9.6p2 g++-8.4.0p25 gcc-8.4.0p25 gcc-libs-8.4.0p25 gmake-4.4.1 ocaml-4.14.2 ocaml-menhir-20230608p1 /usr/sbin/pkg_add -aI -Drepair coq-8.13.2p6 findlib-1.9.6p2 g++-8.4.0p25 gcc-8.4.0p25 gcc-libs-8.4.0p25 gmake-4.4.1 ocaml-4.14.2 ocaml-menhir-20230608p1 >>> Running show-prepare-results in lang/compcert at 1735045958.97 ===> lang/compcert ===> Building from scratch compcert-3.13.1p1 ===> compcert-3.13.1p1 depends on: ocaml->=4.05 -> ocaml-4.14.2 ===> compcert-3.13.1p1 depends on: coq->=8.12.0 -> coq-8.13.2p6 ===> compcert-3.13.1p1 depends on: findlib-* -> findlib-1.9.6p2 ===> compcert-3.13.1p1 depends on: ocaml-menhir->=20190626 -> ocaml-menhir-20230608p1 ===> compcert-3.13.1p1 depends on: gcc->=8,<9 -> gcc-8.4.0p25 ===> compcert-3.13.1p1 depends on: g++->=8,<9 -> g++-8.4.0p25 ===> compcert-3.13.1p1 depends on: gmake-* -> gmake-4.4.1 ===> compcert-3.13.1p1 depends on: gcc-libs->=8,<9 -> gcc-libs-8.4.0p25 ===> Verifying specs: c m estdc++>=19 ===> found c.100.3 m.10.1 estdc++.19.0 coq-8.13.2p6 findlib-1.9.6p2 g++-8.4.0p25 gcc-8.4.0p25 gcc-libs-8.4.0p25 gmake-4.4.1 ocaml-4.14.2 ocaml-menhir-20230608p1 Still tainted: no >>> Running junk in lang/compcert at 1735045960.65 /usr/sbin/pkg_delete -aIXq OpenEXR-3.3.2 akonadi-24.08.3 akonadi-calendar-24.08.3 akonadi-contacts-24.08.3 akonadi-mime-24.08.3 akonadi-notes-24.08.3 akonadi-search-24.08.3 alembic-1.8.5 boost-1.84.0p5v0 cmake-3.31.2v1 coq-8.13.2p6 cyrus-sasl-2.1.28 dbus-1.16.0v0 dwz-0.15 ffmpeg-6.1.2v1 fftw3-3.3.10p0 findlib-1.9.6p2 g++-8.4.0p25 gcc-8.4.0p25 gcc-libs-8.4.0p25 gettext-tools-0.23 glew-2.2.0p0 gmake-4.4.1 gmpxx-6.3.0 gpgme-1.24.1 gpgme-qt-1.24.1 grantleetheme-24.08.3 icu4c-76.1v0 jack-0.125.0p4 jpeg-3.1.0v0 kcalutils-24.08.3 kf6-attica-6.8.0 kf6-baloo-6.8.0 kf6-extra-cmake-modules-6.8.0p0 kf6-karchive-6.8.0 kf6-kauth-6.8.0 kf6-kbookmarks-6.8.0 kf6-kcalendarcore-6.8.0 kf6-kcmutils-6.8.0 kf6-kcodecs-6.8.0 kf6-kcolorscheme-6.8.0 kf6-kcompletion-6.8.0 kf6-kconfig-6.8.0 kf6-kconfigwidgets-6.8.0 kf6-kcontacts-6.8.0 kf6-kcoreaddons-6.8.0 kf6-kcrash-6.8.0 kf6-kdav-6.8.0 kf6-kdbusaddons-6.8.0 kf6-kdeclarative-6.8.0 kf6-kdoctools-6.8.0 kf6-kfilemetadata-6.8.0 kf6-kglobalaccel-6.8.0 kf6-kguiaddons-6.8.0 kf6-kholidays-6.8.0 kf6-ki18n-6.8.0p0 kf6-kiconthemes-6.8.0 kf6-kidletime-6.8.0 kf6-kio-6.8.0 kf6-kirigami-6.8.0 kf6-kitemmodels-6.8.0 kf6-kitemviews-6.8.0 kf6-kjobwidgets-6.8.0 kf6-knewstuff-6.8.0 kf6-knotifications-6.8.0 kf6-knotifyconfig-6.8.0 kf6-kpackage-6.8.0 kf6-kparts-6.8.0 kf6-kquickcharts-6.8.0 kf6-krunner-6.8.0 kf6-kservice-6.8.0 kf6-kstatusnotifieritem-6.8.0 kf6-ksvg-6.8.0 kf6-ktexteditor-6.8.0 kf6-ktexttemplate-6.8.0 kf6-ktextwidgets-6.8.0 kf6-kunitconversion-6.8.0 kf6-kuserfeedback-6.8.0 kf6-kwallet-6.8.0 kf6-kwayland-6.2.4 kf6-kwidgetsaddons-6.8.0 kf6-kwindowsystem-6.8.0 kf6-kxmlgui-6.8.0 kf6-libkexiv2-24.08.3 kf6-libkscreen-6.2.4 kf6-prison-6.8.0 kf6-qqc2-desktop-style-6.8.0 kf6-solid-6.8.0 kf6-sonnet-6.8.0 kf6-syntax-highlighting-6.8.0 kidentitymanagement-24.08.3 kimap-24.08.3 kirigami-addons-1.4.0p0 kldap-24.08.3 kmailtransport-24.08.3 kmbox-24.08.3 kmime-24.08.3 kontactinterface-24.08.3 kpimtextedit-24.08.3 kscreenlocker-6.2.4 ktextaddons-1.5.4 ktnef-24.08.3 kwin-6.2.4p0 layer-shell-qt-6.2.4 libassuan-2.5.5 libcanberra-0.30p6 libgravatar-24.08.3 libkdepim-24.08.3 libkgapi-24.08.3 libkleo-24.08.3 libksieve-24.08.3 libksysguard-6.2.4 libplasma-6.2.4 libqalculate-5.2.0 libsndfile-1.2.2p0 libudev-openbsd-20230921p0 libxkbcommon-1.7.0 mailcommon-24.08.3 messagelib-24.08.3 mimetreeparser-24.08.3 mlt7-7.24.0p0 ninja-1.11.1p0v0 ocaml-4.14.2 ocaml-menhir-20230608p1 openal-1.23.1v0 opencolorio-2.4.0p0v2 openimageio-2.5.13.1p1 openjp2-2.5.3 opensubdiv-3.6.0 openvdb-11.0.0 phonon-qt6-4.12.0p0 pimcommon-24.08.3 plasma-activities-6.2.4 plasma-activities-stats-6.2.4 plasma5support-6.2.4 png-1.6.44 potrace-1.16p0 py3-numpy-1.26.4p2 py3-requests-2.32.2p0 py3-setuptools-69.5.1p0v0 py3-sip-6.8.6p0v0 py3-six-1.17.0p0 python-3.12.8p0 qca-qt6-2.3.9p0 qcoro-qt6-0.11.0p0 qt6-qtbase-6.7.3p0 qt6-qtcharts-6.7.3 qt6-qtdeclarative-6.7.3p0 qt6-qtmultimedia-6.7.3p0 qt6-qtnetworkauth-6.7.3 qt6-qtpositioning-6.7.3 qt6-qtspeech-6.7.3 qt6-qtsvg-6.7.3 qt6-qttools-6.7.3p0 qt6-qtwayland-6.7.3 qt6-qtwebchannel-6.7.3 qt6-qtwebengine-6.7.3p3 qt6-qtwebsockets-6.7.3 qtkeychain-qt6-0.14.2p0 sdl2-2.30.10 shared-mime-info-2.4p0 tbb-2021.13.0p1 tiff-4.7.0p0 vulkan-loader-1.3.296.0 wayland-1.23.1 wxWidgets-gtk3-3.2.6p1 wxWidgets-media-3.2.6p0 wxWidgets-webview-3.2.6p0 xdotool-3.20211022.1v0 xz-5.6.3 --- -jdk-1.8.0.432.b06.1v0 ------------------- You may wish to remove /usr/local/jdk-1.8.0/man from man.conf --- -libmaxminddb-1.11.0 ------------------- You should also run rm /var/db/GeoIP/* --- -ruby-3.3.6 ------------------- If you set up the symlinks to make ruby 3.3 the system ruby, don't forget to remove the following files: rm /usr/local/bin/ruby rm /usr/local/bin/bundle rm /usr/local/bin/bundler rm /usr/local/bin/erb rm /usr/local/bin/gem rm /usr/local/bin/irb rm /usr/local/bin/racc rm /usr/local/bin/rake rm /usr/local/bin/rbs rm /usr/local/bin/rdbg rm /usr/local/bin/rdoc rm /usr/local/bin/ri rm /usr/local/bin/syntax_suggest rm /usr/local/bin/typeprof (Junk lock released for exopi-6 at 1735045988.24) Woken up math/minisat distfiles size=2798512 >>> Running patch in lang/compcert at 1735045988.28 ===> lang/compcert ===> Checking files for compcert-3.13.1p1 `/exopi-cvs/ports/distfiles/CompCert-3.13.1.tar.gz' is up to date. >> (SHA256) all files: OK ===> Extracting for compcert-3.13.1p1 ===> Patching for compcert-3.13.1p1 ===> Applying OpenBSD patch patch-Makefile Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Convenience test target | |Index: Makefile |--- Makefile.orig |+++ Makefile -------------------------- Patching file Makefile using Plan A... Hunk #1 succeeded at 229. Hunk #2 succeeded at 341. done ===> Applying OpenBSD patch patch-configure Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Add configuration support for macppc and aarch64 on OpenBSD | |Index: configure |--- configure.orig |+++ configure -------------------------- Patching file configure using Plan A... Hunk #1 succeeded at 43. Hunk #2 succeeded at 61. Hunk #3 succeeded at 70. Hunk #4 succeeded at 235. Hunk #5 succeeded at 268. Hunk #6 succeeded at 300. Hunk #7 succeeded at 417. done ===> Compiler link: gcc -> /usr/local/bin/egcc ===> Compiler link: cc -> /usr/local/bin/egcc ===> Compiler link: c++ -> /usr/local/bin/eg++ ===> Compiler link: g++ -> /usr/local/bin/eg++ ===> Compiler link: clang -> /usr/bin/clang ===> Compiler link: clang++ -> /usr/bin/clang++ >>> Running configure in lang/compcert at 1735045988.94 ===> lang/compcert ===> Generating configure for compcert-3.13.1p1 ===> Configuring for compcert-3.13.1p1 Testing assembler support for CFI directives... yes Testing linker support for '-no-pie' / '-nopie' option... yes, '-no-pie' Testing Coq... version 8.13.2 -- good! Testing OCaml... version 4.14.2 -- good! Testing OCaml native-code compiler... yes Testing OCaml .opt compilers... yes Testing Menhir... version 20230608 -- good! Testing GNU make... version 4.4.1 (command 'gmake') -- good! CompCert configuration: Target architecture........... x86 Hardware model................ 64 Application binary interface.. standard Endianness.................... little OS and development env........ bsd C compiler.................... egcc -m64 C preprocessor................ egcc -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E Assembler..................... egcc -m64 -c Assembler supports CFI........ true Assembler for runtime lib..... egcc -m64 -c Linker........................ egcc -m64 -no-pie Archiver...................... ar rcs Math library.................. -lm Build command to use.......... gmake Menhir API library............ /usr/local/lib/ocaml/menhirLib The Flocq library............. local The MenhirLib library......... local Binaries installed in......... /usr/local/bin Shared config installed in.... /usr/local/share/compcert Runtime library provided...... true Library files installed in.... /usr/local/lib Man pages installed in........ /usr/local/man Standard headers provided..... false Standard headers installed in. /usr/local/lib/include Coq development will not be installed >>> Running build in lang/compcert at 1735045989.93 ===> lang/compcert ===> Building for compcert-3.13.1p1 gmake[1]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml Preprocessing x86/ConstpropOp.vp Preprocessing x86/SelectOp.vp Preprocessing x86/SelectLong.vp Preprocessing backend/SelectDiv.vp Preprocessing backend/SplitLong.vp menhir --coq --coq-no-version-check cparser/Parser.vy Analyzing Coq dependencies gmake[1]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' gmake proof gmake[1]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' COQC lib/Axioms.v COQC lib/Coqlib.v COQC lib/Intv.v COQC lib/Maps.v COQC lib/Zbits.v COQC flocq/Core/Zaux.v COQC flocq/Core/Raux.v COQC flocq/Core/Defs.v COQC flocq/Core/Digits.v COQC flocq/Core/Float_prop.v COQC flocq/Core/Round_pred.v COQC flocq/Core/Generic_fmt.v COQC flocq/Core/Ulp.v COQC flocq/Core/Round_NE.v COQC flocq/Core/FIX.v COQC flocq/Core/FLX.v COQC flocq/Core/FLT.v COQC flocq/Core/Core.v COQC flocq/Calc/Bracket.v COQC flocq/Calc/Round.v COQC flocq/Calc/Operations.v COQC flocq/Calc/Div.v COQC flocq/Calc/Sqrt.v COQC flocq/Prop/Relative.v COQC flocq/IEEE754/BinarySingleNaN.v COQC flocq/IEEE754/Binary.v COQC flocq/IEEE754/Bits.v COQC x86_64/Archi.v COQC lib/Integers.v COQC lib/Ordered.v COQC lib/Heaps.v COQC lib/Lattice.v COQC lib/Wfsimpl.v COQC lib/Iteration.v COQC flocq/Prop/Sterbenz.v COQC flocq/Prop/Round_odd.v COQC lib/IEEE754_extra.v COQC lib/Floats.v COQC lib/Parmov.v COQC lib/UnionFind.v COQC lib/Postorder.v COQC lib/FSetAVLplus.v COQC lib/IntvSets.v COQC lib/Decidableplus.v COQC lib/BoolEqual.v COQC common/Errors.v COQC common/AST.v COQC common/Linking.v COQC common/Values.v COQC common/Memdata.v COQC common/Memtype.v COQC common/Memory.v COQC common/Globalenvs.v COQC common/Builtins0.v COQC x86/Builtins1.v COQC common/Builtins.v COQC common/Events.v COQC common/Smallstep.v COQC common/Behaviors.v COQC common/Switch.v COQC common/Determinism.v COQC common/Unityping.v COQC common/Separation.v COQC backend/Cminor.v COQC backend/Cminortyping.v COQC x86/Op.v COQC backend/CminorSel.v COQC driver/Compopts.v COQC x86/SelectOp.v COQC backend/SplitLong.v COQC x86/SelectLong.v COQC backend/SelectDiv.v COQC x86/Machregs.v COQC backend/Selection.v COQC x86/SelectOpproof.v COQC backend/SplitLongproof.v COQC x86/SelectLongproof.v COQC backend/SelectDivproof.v COQC backend/Selectionproof.v COQC backend/Registers.v COQC backend/RTL.v COQC backend/RTLgen.v COQC backend/RTLgenspec.v COQC backend/RTLgenproof.v COQC backend/Locations.v COQC x86/Conventions1.v COQC backend/Conventions.v COQC backend/Tailcall.v COQC backend/Tailcallproof.v COQC backend/Inlining.v COQC backend/Inliningspec.v COQC backend/Inliningproof.v COQC backend/Renumber.v COQC backend/Renumberproof.v COQC backend/RTLtyping.v COQC backend/Kildall.v COQC backend/Liveness.v COQC backend/ValueDomain.v COQC x86/ValueAOp.v COQC backend/ValueAnalysis.v COQC x86/ConstpropOp.v COQC backend/Constprop.v COQC x86/ConstpropOpproof.v COQC backend/Constpropproof.v COQC backend/CSEdomain.v COQC x86/CombineOp.v COQC backend/CSE.v COQC x86/CombineOpproof.v COQC backend/CSEproof.v COQC backend/NeedDomain.v COQC x86/NeedOp.v COQC backend/Deadcode.v COQC backend/Deadcodeproof.v COQC backend/Unusedglob.v COQC backend/Unusedglobproof.v COQC backend/LTL.v COQC backend/Allocation.v COQC backend/Allocproof.v COQC backend/Tunneling.v COQC backend/Tunnelingproof.v COQC backend/Linear.v COQC backend/Lineartyping.v COQC backend/Linearize.v COQC backend/Linearizeproof.v COQC backend/CleanupLabels.v COQC backend/CleanupLabelsproof.v COQC backend/Debugvar.v COQC backend/Debugvarproof.v COQC backend/Bounds.v COQC x86/Stacklayout.v COQC backend/Mach.v COQC backend/Stacking.v COQC backend/Stackingproof.v COQC x86/Asm.v COQC x86/Asmgen.v COQC backend/Asmgenproof0.v COQC x86/Asmgenproof1.v COQC x86/Asmgenproof.v COQC cfrontend/Ctypes.v COQC cfrontend/Cop.v COQC cfrontend/Csyntax.v COQC cfrontend/Csem.v COQC cfrontend/Ctyping.v COQC cfrontend/Cstrategy.v COQC cfrontend/Cexec.v COQC cfrontend/Initializers.v COQC cfrontend/Initializersproof.v COQC cfrontend/Clight.v COQC cfrontend/SimplExpr.v COQC cfrontend/SimplExprspec.v COQC cfrontend/SimplExprproof.v COQC cfrontend/ClightBigstep.v COQC cfrontend/SimplLocals.v COQC cfrontend/SimplLocalsproof.v COQC cfrontend/Csharpminor.v COQC cfrontend/Cshmgen.v COQC cfrontend/Cshmgenproof.v COQC cfrontend/Cminorgen.v COQC cfrontend/Cminorgenproof.v COQC driver/Compiler.v COQC driver/Complements.v COQC flocq/Core/FTZ.v COQC flocq/Calc/Plus.v COQC flocq/Prop/Plus_error.v COQC flocq/Prop/Mult_error.v COQC flocq/Prop/Div_sqrt_error.v COQC flocq/Prop/Double_rounding.v COQC MenhirLib/Alphabet.v COQC MenhirLib/Grammar.v COQC MenhirLib/Automaton.v COQC MenhirLib/Validator_classes.v COQC MenhirLib/Validator_safe.v COQC MenhirLib/Interpreter.v COQC MenhirLib/Validator_complete.v COQC MenhirLib/Interpreter_complete.v COQC MenhirLib/Interpreter_correct.v COQC MenhirLib/Main.v COQC cparser/Cabs.v COQC cparser/Parser.v gmake[1]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' gmake extraction gmake[1]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' rm -f extraction/*.ml extraction/*.mli "coqtop" -R lib compcert.lib -R common compcert.common -R x86_64 compcert.x86_64 -R x86 compcert.x86 -R backend compcert.backend -R cfrontend compcert.cfrontend -R driver compcert.driver -R export compcert.export -R cparser compcert.cparser -R flocq Flocq -R MenhirLib MenhirLib -batch -load-vernac-source extraction/extraction.v File "/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/extraction/extraction.v", line 154, characters 0-1147: Warning: The extraction is currently set to bypass opacity, the following opaque constant bodies have been accessed : solve_constraints_terminate. [extraction-opaque-accessed,extraction] touch extraction/STAMP gmake[1]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' gmake ccomp gmake[1]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' ocamlopt -o tools/modorder str.cmxa tools/modorder.ml (echo 'let version = "3.13"'; \ echo 'let buildnr = ""'; \ echo 'let tag = ""'; \ echo 'let branch = ""') > driver/Version.ml gmake -f Makefile.extr depend gmake[2]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' menhir --table -v --no-stdlib -la 1 cparser/pre_parser.mly Built an LR(0) automaton with 628 states. The construction mode is pager. Built an LR(1) automaton with 628 states. 2 shift/reduce conflicts were silently solved. Extra reductions on error were added in 103 states. Priority played a role in 0 of these states. ocamllex -q cparser/Lexer.mll ocamllex -q lib/Tokenize.mll ocamllex -q lib/Readconfig.mll ocamllex -q lib/Responsefile.mll gmake -C cparser correct gmake[3]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/cparser' Built an LR(0) automaton with 628 states. The construction mode is pager. Built an LR(1) automaton with 628 states. 2 shift/reduce conflicts were silently solved. Extra reductions on error were added in 103 states. Priority played a role in 0 of these states. Read 233 sample input sentences and 180 error messages. OK. The set of erroneous inputs is correct and irredundant. gmake[3]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/cparser' Analyzing OCaml dependencies gmake[2]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' (echo "stdlib_path=/usr/local/lib"; \ echo "prepro=egcc"; \ echo "linker=egcc"; \ echo "asm=egcc"; \ echo "prepro_options=-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E";\ echo "asm_options=-m64 -c";\ echo "linker_options=-m64 -no-pie";\ echo "arch=x86"; \ echo "model=64"; \ echo "abi=standard"; \ echo "endianness=little"; \ echo "system=bsd"; \ echo "has_runtime_lib=true"; \ echo "has_standard_headers=false"; \ echo "asm_supports_cfi=true"; \ echo "response_file_style=gnu";) \ > compcert.ini gmake -f Makefile.extr ccomp gmake[2]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' OCAMLOPT driver/Version.ml OCAMLC lib/Readconfig.mli OCAMLOPT lib/Readconfig.ml OCAMLC lib/Responsefile.mli OCAMLOPT lib/Responsefile.ml OCAMLC lib/Commandline.mli OCAMLOPT lib/Commandline.ml OCAMLC driver/Configuration.mli OCAMLOPT driver/Configuration.ml OCAMLOPT driver/Clflags.ml OCAMLC extraction/Datatypes.mli OCAMLOPT extraction/Datatypes.ml OCAMLC extraction/Nat.mli OCAMLOPT extraction/Nat.ml OCAMLC extraction/BinNums.mli OCAMLOPT extraction/BinNums.ml OCAMLC extraction/BinPosDef.mli OCAMLOPT extraction/BinPosDef.ml OCAMLC extraction/BinPos.mli OCAMLOPT extraction/BinPos.ml OCAMLC extraction/Zpower.mli OCAMLOPT extraction/Zpower.ml OCAMLC extraction/BinNat.mli OCAMLOPT extraction/BinNat.ml OCAMLC extraction/BinInt.mli OCAMLOPT extraction/BinInt.ml OCAMLC extraction/ZArith_dec.mli OCAMLOPT extraction/ZArith_dec.ml OCAMLC extraction/List0.mli OCAMLOPT extraction/List0.ml OCAMLC extraction/Coqlib.mli OCAMLOPT extraction/Coqlib.ml OCAMLC extraction/Zbits.mli OCAMLOPT extraction/Zbits.ml OCAMLC extraction/Archi.mli OCAMLOPT extraction/Archi.ml OCAMLC extraction/Integers.mli OCAMLOPT extraction/Integers.ml OCAMLC extraction/Zaux.mli OCAMLOPT extraction/Zaux.ml OCAMLC extraction/Zbool.mli OCAMLOPT extraction/Zbool.ml OCAMLC extraction/SpecFloat.mli OCAMLOPT extraction/SpecFloat.ml OCAMLC extraction/Round.mli OCAMLOPT extraction/Round.ml OCAMLC extraction/Bool.mli OCAMLOPT extraction/Bool.ml OCAMLC extraction/BinarySingleNaN.mli OCAMLOPT extraction/BinarySingleNaN.ml OCAMLC extraction/Binary.mli OCAMLOPT extraction/Binary.ml OCAMLC extraction/IEEE754_extra.mli OCAMLOPT extraction/IEEE754_extra.ml OCAMLC extraction/Bits.mli OCAMLOPT extraction/Bits.ml OCAMLC extraction/Floats.mli OCAMLOPT extraction/Floats.ml OCAMLOPT lib/Camlcoq.ml OCAMLOPT driver/Timing.ml OCAMLC extraction/Orders.mli OCAMLOPT extraction/Orders.ml OCAMLC extraction/OrdersTac.mli OCAMLOPT extraction/OrdersTac.ml OCAMLC extraction/OrderedType.mli OCAMLOPT extraction/OrderedType.ml OCAMLC extraction/EquivDec.mli OCAMLOPT extraction/EquivDec.ml OCAMLC extraction/Maps.mli OCAMLOPT extraction/Maps.ml OCAMLC extraction/Ordered.mli OCAMLOPT extraction/Ordered.ml OCAMLC extraction/Int0.mli OCAMLOPT extraction/Int0.ml OCAMLC extraction/OrdersAlt.mli OCAMLOPT extraction/OrdersAlt.ml OCAMLC extraction/OrdersFacts.mli OCAMLOPT extraction/OrdersFacts.ml OCAMLC extraction/MSetInterface.mli OCAMLOPT extraction/MSetInterface.ml OCAMLC extraction/MSetAVL.mli OCAMLOPT extraction/MSetAVL.ml OCAMLC extraction/FSetAVL.mli OCAMLOPT extraction/FSetAVL.ml OCAMLC extraction/Registers.mli OCAMLOPT extraction/Registers.ml OCAMLC extraction/BoolEqual.mli OCAMLOPT extraction/BoolEqual.ml OCAMLC extraction/String0.mli OCAMLOPT extraction/String0.ml OCAMLC extraction/Errors.mli OCAMLOPT extraction/Errors.ml OCAMLC extraction/AST.mli OCAMLOPT extraction/AST.ml OCAMLC extraction/Op.mli OCAMLOPT extraction/Op.ml OCAMLC extraction/Machregs.mli OCAMLOPT extraction/Machregs.ml OCAMLC extraction/Locations.mli OCAMLOPT extraction/Locations.ml OCAMLC lib/Camlcoq.ml OCAMLC backend/XTL.mli OCAMLOPT backend/XTL.ml OCAMLC extraction/RTL.mli OCAMLOPT extraction/RTL.ml OCAMLC extraction/Equalities.mli OCAMLOPT extraction/Equalities.ml OCAMLC extraction/DecidableType.mli OCAMLOPT extraction/DecidableType.ml OCAMLC extraction/FSetInterface.mli OCAMLOPT extraction/FSetInterface.ml OCAMLC extraction/Lattice.mli OCAMLOPT extraction/Lattice.ml OCAMLC extraction/Specif.mli OCAMLOPT extraction/Specif.ml OCAMLC extraction/Iteration.mli OCAMLOPT extraction/Iteration.ml OCAMLC extraction/Heaps.mli OCAMLOPT extraction/Heaps.ml OCAMLC extraction/Kildall.mli OCAMLOPT extraction/Kildall.ml OCAMLOPT backend/Splitting.ml OCAMLC extraction/Unityping.mli OCAMLOPT extraction/Unityping.ml OCAMLC extraction/Conventions1.mli OCAMLOPT extraction/Conventions1.ml OCAMLC extraction/Conventions.mli OCAMLOPT extraction/Conventions.ml OCAMLC extraction/RTLtyping.mli OCAMLOPT extraction/RTLtyping.ml OCAMLOPT common/PrintAST.ml OCAMLOPT x86/PrintOp.ml OCAMLC backend/Machregsnames.mli OCAMLOPT backend/Machregsnames.ml OCAMLOPT backend/PrintXTL.ml OCAMLC extraction/LTL.mli OCAMLOPT extraction/LTL.ml OCAMLOPT backend/PrintLTL.ml OCAMLC lib/Tokenize.mli OCAMLOPT lib/Tokenize.ml OCAMLC cparser/Diagnostics.mli OCAMLOPT cparser/Diagnostics.ml OCAMLC cparser/C.mli OCAMLC cparser/Machine.mli OCAMLOPT cparser/Machine.ml OCAMLC cparser/Env.mli OCAMLOPT cparser/Env.ml OCAMLC cparser/Cprint.mli OCAMLOPT cparser/Cprint.ml OCAMLC cparser/Cutil.mli OCAMLOPT cparser/Cutil.ml OCAMLC common/Sections.mli OCAMLOPT common/Sections.ml OCAMLC extraction/Values.mli OCAMLOPT extraction/Values.ml OCAMLC extraction/Znumtheory.mli OCAMLOPT extraction/Znumtheory.ml OCAMLC extraction/Memtype.mli OCAMLOPT extraction/Memtype.ml OCAMLC extraction/PeanoNat.mli OCAMLOPT extraction/PeanoNat.ml OCAMLC extraction/Memdata.mli OCAMLOPT extraction/Memdata.ml OCAMLC extraction/Memory.mli OCAMLOPT extraction/Memory.ml OCAMLC extraction/Ctypes.mli OCAMLOPT extraction/Ctypes.ml OCAMLC extraction/Cop.mli OCAMLOPT extraction/Cop.ml OCAMLC extraction/Csyntax.mli OCAMLOPT extraction/Csyntax.ml OCAMLC extraction/Initializers.mli OCAMLOPT extraction/Initializers.ml OCAMLC x86/Machregsaux.mli OCAMLOPT x86/Machregsaux.ml OCAMLC cparser/Ceval.mli OCAMLOPT cparser/Ceval.ml OCAMLOPT x86/CBuiltins.ml OCAMLOPT cparser/ExtendedAsm.ml OCAMLC debug/DwarfTypes.mli OCAMLC debug/Debug.mli OCAMLOPT debug/Debug.ml OCAMLC extraction/Ctyping.mli OCAMLOPT extraction/Ctyping.ml OCAMLC backend/AisAnnot.mli OCAMLOPT backend/AisAnnot.ml OCAMLOPT cfrontend/C2C.ml OCAMLOPT cfrontend/CPragmas.ml OCAMLC backend/IRC.mli OCAMLOPT backend/IRC.ml OCAMLOPT backend/Regalloc.ml OCAMLOPT backend/PrintRTL.ml OCAMLC extraction/Mach.mli OCAMLOPT extraction/Mach.ml OCAMLOPT backend/PrintMach.ml OCAMLOPT cfrontend/PrintCsyntax.ml OCAMLC extraction/Cminor.mli OCAMLOPT extraction/Cminor.ml OCAMLOPT backend/PrintCminor.ml OCAMLC extraction/Clight.mli OCAMLOPT extraction/Clight.ml OCAMLOPT cfrontend/PrintClight.ml OCAMLC extraction/Asm.mli OCAMLOPT extraction/Asm.ml OCAMLOPT backend/PrintAsmaux.ml OCAMLC lib/Printlines.mli OCAMLOPT lib/Printlines.ml OCAMLOPT backend/Fileinfo.ml OCAMLOPT x86/TargetPrinter.ml OCAMLOPT debug/DwarfUtil.ml OCAMLC debug/DwarfPrinter.mli OCAMLOPT debug/DwarfPrinter.ml OCAMLC backend/PrintAsm.mli OCAMLOPT backend/PrintAsm.ml OCAMLC driver/Driveraux.mli OCAMLOPT driver/Driveraux.ml OCAMLC driver/Linker.mli OCAMLOPT driver/Linker.ml OCAMLC extraction/Globalenvs.mli OCAMLOPT extraction/Globalenvs.ml OCAMLC extraction/Events.mli OCAMLOPT extraction/Events.ml OCAMLC extraction/Determinism.mli OCAMLOPT extraction/Determinism.ml OCAMLC extraction/Csem.mli OCAMLOPT extraction/Csem.ml OCAMLC extraction/DecidableClass.mli OCAMLOPT extraction/DecidableClass.ml OCAMLC extraction/Decidableplus.mli OCAMLOPT extraction/Decidableplus.ml OCAMLC extraction/Builtins0.mli OCAMLOPT extraction/Builtins0.ml OCAMLC extraction/Builtins1.mli OCAMLOPT extraction/Builtins1.ml OCAMLC extraction/Builtins.mli OCAMLOPT extraction/Builtins.ml OCAMLC extraction/Cexec.mli OCAMLOPT extraction/Cexec.ml OCAMLOPT driver/Interp.ml OCAMLC cparser/Unblock.mli OCAMLOPT cparser/Unblock.ml OCAMLC cparser/Transform.mli OCAMLOPT cparser/Transform.ml OCAMLC cparser/SwitchNorm.mli OCAMLOPT cparser/SwitchNorm.ml OCAMLC cparser/StructPassing.mli OCAMLOPT cparser/StructPassing.ml OCAMLC cparser/Rename.mli OCAMLOPT cparser/Rename.ml OCAMLC extraction/Alphabet.mli OCAMLOPT extraction/Alphabet.ml OCAMLC extraction/Grammar.mli OCAMLOPT extraction/Grammar.ml OCAMLC extraction/Automaton.mli OCAMLOPT extraction/Automaton.ml OCAMLC extraction/Interpreter_correct.mli OCAMLOPT extraction/Interpreter_correct.ml OCAMLC extraction/FMapList.mli OCAMLOPT extraction/FMapList.ml OCAMLC extraction/FMapAVL.mli OCAMLOPT extraction/FMapAVL.ml OCAMLC extraction/Validator_complete.mli OCAMLOPT extraction/Validator_complete.ml OCAMLC extraction/Interpreter_complete.mli OCAMLOPT extraction/Interpreter_complete.ml OCAMLC extraction/Validator_safe.mli OCAMLOPT extraction/Validator_safe.ml OCAMLC extraction/Interpreter.mli OCAMLOPT extraction/Interpreter.ml OCAMLC extraction/Main.mli OCAMLOPT extraction/Main.ml OCAMLC extraction/Cabs.mli OCAMLOPT extraction/Cabs.ml OCAMLC extraction/Parser.mli OCAMLOPT extraction/Parser.ml OCAMLOPT cparser/PackedStructs.ml OCAMLC cparser/pre_parser_aux.mli OCAMLOPT cparser/pre_parser_aux.ml OCAMLC cparser/pre_parser.mli OCAMLOPT cparser/pre_parser.ml OCAMLOPT cparser/pre_parser_messages.ml OCAMLC cparser/ErrorReports.mli OCAMLOPT cparser/ErrorReports.ml OCAMLOPT cparser/Lexer.ml OCAMLC cparser/Cleanup.mli OCAMLOPT cparser/Cleanup.ml OCAMLC cparser/Checks.mli OCAMLOPT cparser/Checks.ml OCAMLC cparser/Cflow.mli OCAMLOPT cparser/Cflow.ml OCAMLOPT cparser/Cabshelper.ml OCAMLC cparser/Elab.mli OCAMLOPT cparser/Elab.ml OCAMLC cparser/Parse.mli OCAMLOPT cparser/Parse.ml OCAMLC driver/Frontend.mli OCAMLOPT driver/Frontend.ml OCAMLC debug/DebugTypes.mli OCAMLC debug/DebugInformation.mli OCAMLOPT debug/DebugInformation.ml OCAMLOPT debug/Dwarfgen.ml OCAMLOPT debug/DebugInit.ml OCAMLC extraction/Unusedglob.mli OCAMLOPT extraction/Unusedglob.ml OCAMLC extraction/UnionFind.mli OCAMLOPT extraction/UnionFind.ml OCAMLC extraction/Tunneling.mli OCAMLOPT extraction/Tunneling.ml OCAMLC extraction/Tailcall.mli OCAMLOPT extraction/Tailcall.ml OCAMLC extraction/Linear.mli OCAMLOPT extraction/Linear.ml OCAMLC extraction/Bounds.mli OCAMLOPT extraction/Bounds.ml OCAMLC extraction/Stacklayout.mli OCAMLOPT extraction/Stacklayout.ml OCAMLC extraction/Lineartyping.mli OCAMLOPT extraction/Lineartyping.ml OCAMLC extraction/Stacking.mli OCAMLOPT extraction/Stacking.ml OCAMLC extraction/Compopts.mli OCAMLOPT extraction/Compopts.ml OCAMLC extraction/SimplLocals.mli OCAMLOPT extraction/SimplLocals.ml OCAMLC extraction/SimplExpr.mli OCAMLOPT extraction/SimplExpr.ml OCAMLC extraction/Switch.mli OCAMLOPT extraction/Switch.ml OCAMLOPT common/Switchaux.ml OCAMLC extraction/Compare_dec.mli OCAMLOPT extraction/Compare_dec.ml OCAMLC extraction/CminorSel.mli OCAMLOPT extraction/CminorSel.ml OCAMLC extraction/SelectOp.mli OCAMLOPT extraction/SelectOp.ml OCAMLC extraction/SplitLong.mli OCAMLOPT extraction/SplitLong.ml OCAMLOPT backend/Selectionaux.ml OCAMLC extraction/SelectLong.mli OCAMLOPT extraction/SelectLong.ml OCAMLC extraction/SelectDiv.mli OCAMLOPT extraction/SelectDiv.ml OCAMLC extraction/Cminortyping.mli OCAMLOPT extraction/Cminortyping.ml OCAMLC extraction/Selection.mli OCAMLOPT extraction/Selection.ml OCAMLC extraction/Mergesort.mli OCAMLOPT extraction/Mergesort.ml OCAMLC extraction/Postorder.mli OCAMLOPT extraction/Postorder.ml OCAMLC extraction/Renumber.mli OCAMLOPT extraction/Renumber.ml OCAMLOPT backend/RTLgenaux.ml OCAMLC extraction/RTLgen.mli OCAMLOPT extraction/RTLgen.ml OCAMLOPT backend/Linearizeaux.ml OCAMLC extraction/Linearize.mli OCAMLOPT extraction/Linearize.ml OCAMLOPT backend/Inliningaux.ml OCAMLC driver/Clflags.ml OCAMLC x86/CBuiltins.ml OCAMLC cparser/ExtendedAsm.ml OCAMLC cfrontend/C2C.ml OCAMLC backend/Inliningaux.ml OCAMLC extraction/Inlining.mli OCAMLOPT extraction/Inlining.ml OCAMLC extraction/Debugvar.mli OCAMLOPT extraction/Debugvar.ml OCAMLC extraction/ValueDomain.mli OCAMLOPT extraction/ValueDomain.ml OCAMLC extraction/ValueAOp.mli OCAMLOPT extraction/ValueAOp.ml OCAMLC extraction/Liveness.mli OCAMLOPT extraction/Liveness.ml OCAMLC extraction/ValueAnalysis.mli OCAMLOPT extraction/ValueAnalysis.ml OCAMLC extraction/IntvSets.mli OCAMLOPT extraction/IntvSets.ml OCAMLC extraction/NeedDomain.mli OCAMLOPT extraction/NeedDomain.ml OCAMLC extraction/NeedOp.mli OCAMLOPT extraction/NeedOp.ml OCAMLC extraction/Deadcode.mli OCAMLOPT extraction/Deadcode.ml OCAMLC extraction/Csharpminor.mli OCAMLOPT extraction/Csharpminor.ml OCAMLC extraction/Cshmgen.mli OCAMLOPT extraction/Cshmgen.ml OCAMLC extraction/ConstpropOp.mli OCAMLOPT extraction/ConstpropOp.ml OCAMLC extraction/Constprop.mli OCAMLOPT extraction/Constprop.ml OCAMLC extraction/Cminorgen.mli OCAMLOPT extraction/Cminorgen.ml OCAMLC extraction/CleanupLabels.mli OCAMLOPT extraction/CleanupLabels.ml OCAMLC extraction/CSEdomain.mli OCAMLOPT extraction/CSEdomain.ml OCAMLC extraction/CombineOp.mli OCAMLOPT extraction/CombineOp.ml OCAMLC extraction/CSE.mli OCAMLOPT extraction/CSE.ml OCAMLC extraction/Asmgen.mli OCAMLOPT extraction/Asmgen.ml OCAMLC extraction/FSetAVLplus.mli OCAMLOPT extraction/FSetAVLplus.ml OCAMLC extraction/Allocation.mli OCAMLOPT extraction/Allocation.ml OCAMLC extraction/Compiler.mli OCAMLOPT extraction/Compiler.ml OCAMLOPT driver/CommonOptions.ml OCAMLC driver/Assembler.mli OCAMLOPT driver/Assembler.ml OCAMLC backend/Asmexpandaux.mli OCAMLOPT backend/Asmexpandaux.ml OCAMLOPT x86/Asmexpand.ml OCAMLC x86/AsmToJSON.mli OCAMLOPT x86/AsmToJSON.ml OCAMLOPT driver/Driver.ml Linking ccomp gmake[2]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' gmake[1]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' gmake runtime gmake[1]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' gmake -C runtime gmake[2]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/runtime' egcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_bsd -o i64_dtou.o x86_64/i64_dtou.S egcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_bsd -o i64_utod.o x86_64/i64_utod.S egcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_bsd -o i64_utof.o x86_64/i64_utof.S egcc -m64 -c -DMODEL_64 -DABI_standard -DENDIANNESS_little -DSYS_bsd -o vararg.o x86_64/vararg.S rm -f libcompcert.a ar rcs libcompcert.a i64_dtou.o i64_utod.o i64_utof.o vararg.o gmake[2]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/runtime' gmake[1]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1' >>> Running fake in lang/compcert at 1735047074.72 ===> lang/compcert ===> Faking installation for compcert-3.13.1p1 install -d /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/bin install -m 0755 ./ccomp /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/bin install -d /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/share/compcert install -m 0644 ./compcert.ini /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/share/compcert install -d /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/man/man1 install -m 0644 ./doc/ccomp.1 /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/man/man1 gmake -C runtime install gmake[1]: Entering directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/runtime' install -d /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/lib install -m 0644 libcompcert.a /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/lib gmake[1]: Leaving directory '/exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/runtime' /exopi-obj/pobj/compcert-3.13.1/bin/install -c -m 644 /exopi-obj/pobj/compcert-3.13.1/CompCert-3.13.1/LICENSE /exopi-obj/pobj/compcert-3.13.1/fake-amd64/usr/local/share/compcert >>> Running package in lang/compcert at 1735047075.42 ===> lang/compcert `/exopi-obj/pobj/compcert-3.13.1/fake-amd64/.fake_done' is up to date. ===> Building package for compcert-3.13.1p1 Create /exopi-cvs/ports/packages/amd64/all/compcert-3.13.1p1.tgz Creating package compcert-3.13.1p1 reading plist| checking dependencies| checking dependencies|lang/gcc/8,-libs checking dependencies|lang/gcc/8,-main checksumming| checksumming| | 0% checksumming|*** | 6% checksumming|******* | 11% checksumming|********** | 17% checksumming|************** | 22% checksumming|***************** | 28% checksumming|******************** | 33% checksumming|************************ | 39% checksumming|*************************** | 44% checksumming|******************************* | 50% checksumming|********************************** | 56% checksumming|************************************* | 61% checksumming|***************************************** | 67% checksumming|******************************************** | 72% checksumming|*********************************************** | 78% checksumming|*************************************************** | 83% checksumming|****************************************************** | 89% checksumming|********************************************************** | 94% checksumming|*************************************************************|100% archiving| archiving| | 0% archiving|*********** | 18% archiving|*********************** | 36% archiving|********************************** | 54% archiving|********************************************** | 71% archiving|********************************************************* | 89% archiving|****************************************************************| 99% archiving|****************************************************************|100% Link to /exopi-cvs/ports/packages/amd64/ftp/compcert-3.13.1p1.tgz >>> Running clean in lang/compcert at 1735047079.07 ===> lang/compcert ===> Cleaning for compcert-3.13.1p1 >>> Ended at 1735047079.56 max_stuck=52.61/depends=34.64/show-prepare-results=1.68/junk=27.62/patch=0.67/configure=1.00/build=1084.77/fake=0.67/package=3.69/clean=0.52