Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq fails to compile when Ocaml is built with -Ofast #840

Open
LemonBreezes opened this issue May 8, 2022 · 0 comments
Open

Coq fails to compile when Ocaml is built with -Ofast #840

LemonBreezes opened this issue May 8, 2022 · 0 comments

Comments

@LemonBreezes
Copy link

The respective packages are:
dev-lang/ocaml-4.14.0:0/4.14::gentoo USE="ocamlopt -emacs -flambda -latex -xemacs"
sci-mathematics/coq-8.15.1::gentoo USE="ocamlopt -debug -doc -gtk"

and my system info is:
Portage 3.0.30 (python 3.9.12-final-0, default/linux/amd64/17.1, gcc-11.3.0, glibc-2.35-r4, 5.17.4-gentoo x86_64)

                     System Settings

=================================================================
System uname: Linux-5.17.4-gentoo-x86_64-Intel-R-_Core-TM-i9-9900K_CPU@_3.60GHz-with-glibc2.35
KiB Mem: 49210600 total, 27035252 free
KiB Swap: 0 total, 0 free
Timestamp of repository gentoo: Sun, 08 May 2022 16:48:51 +0000
Head commit of repository gentoo: ac190c307cbe5941e71f21ae7c0b181d23f310eb

sh bash 5.1_p16
ld GNU ld (Gentoo 2.38 p4) 2.38
ccache version 4.6 [disabled]
app-misc/pax-utils: 1.3.4::gentoo
app-shells/bash: 5.1_p16::gentoo
dev-lang/perl: 5.34.1-r3::gentoo
dev-lang/python: 3.9.12::gentoo, 3.10.4::gentoo
dev-lang/rust: 1.60.0::gentoo
dev-util/ccache: 4.6-r1::gentoo
dev-util/cmake: 3.23.1::gentoo
dev-util/meson: 0.61.4-r2::gentoo
sys-apps/baselayout: 2.8::gentoo
sys-apps/openrc: 0.44.10::gentoo
sys-apps/sandbox: 2.29::gentoo
sys-devel/autoconf: 2.71-r1::gentoo
sys-devel/automake: 1.16.5::gentoo
sys-devel/binutils: 2.38-r2::gentoo
sys-devel/binutils-config: 5.4.1::gentoo
sys-devel/gcc: 11.3.0::gentoo
sys-devel/gcc-config: 2.5-r1::gentoo
sys-devel/libtool: 2.4.7::gentoo
sys-devel/llvm: 14.0.3::gentoo
sys-devel/make: 4.3::gentoo
sys-kernel/linux-headers: 5.17-r1::gentoo (virtual/os-headers)
sys-libs/glibc: 2.35-r4::gentoo
Repositories:

gentoo
location: /var/db/repos/gentoo
sync-type: git
sync-uri: git://anongit.gentoo.org/repo/sync/gentoo.git
priority: -1000
sync-git-verify-commit-signature: yes

guru
location: /var/lib/layman/guru
masters: gentoo
priority: 50

lto-overlay
location: /var/lib/layman/lto-overlay
masters: gentoo mv
priority: 50

mv
location: /var/lib/layman/mv
masters: gentoo
priority: 50

robertgzr
location: /var/lib/layman/robertgzr
masters: gentoo
priority: 50

ACCEPT_KEYWORDS="amd64 ~amd64"
ACCEPT_LICENSE="@free"
CBUILD="x86_64-pc-linux-gnu"
CFLAGS="-march=native -Ofast -fgraphite-identity -floop-nest-optimize -fdevirtualize-at-ltrans -fipa-pta -fno-semantic-interposition -flto=16 -fuse-linker-plugin -falign-functions=32 -pipe"
CHOST="x86_64-pc-linux-gnu"
CONFIG_PROTECT="/etc /usr/share/gnupg/qualified.txt"
CONFIG_PROTECT_MASK="/etc/ca-certificates.conf /etc/env.d /etc/fonts/fonts.conf /etc/gconf /etc/gentoo-release /etc/revdep-rebuild /etc/sandbox.d /etc/terminfo"
CXXFLAGS="-march=native -Ofast -fgraphite-identity -floop-nest-optimize -fdevirtualize-at-ltrans -fipa-pta -fno-semantic-interposition -flto=16 -fuse-linker-plugin -falign-functions=32 -pipe"
DISTDIR="/var/cache/distfiles"
EMERGE_DEFAULT_OPTS="--jobs=16 --load-average=16"
ENV_UNSET="CARGO_HOME DBUS_SESSION_BUS_ADDRESS DISPLAY GOBIN GOPATH PERL5LIB PERL5OPT PERLPREFIX PERL_CORE PERL_MB_OPT PERL_MM_OPT XAUTHORITY XDG_CACHE_HOME XDG_CONFIG_HOME XDG_DATA_HOME XDG_RUNTIME_DIR"
FCFLAGS="-march=native -Ofast -fgraphite-identity -floop-nest-optimize -fdevirtualize-at-ltrans -fipa-pta -fno-semantic-interposition -flto=16 -fuse-linker-plugin -falign-functions=32 -pipe"
FEATURES="assume-digests binpkg-docompress binpkg-dostrip binpkg-logs binpkg-multi-instance buildpkg-live config-protect-if-modified distlocks ebuild-locks fixlafiles ipc-sandbox merge-sync multilib-strict network-sandbox news parallel-fetch parallel-install pid-sandbox preserve-libs protect-owned qa-unresolved-soname-deps sandbox sfperms strict unknown-features-warn unmerge-logs unmerge-orphans userfetch userpriv usersandbox usersync xattr"
FFLAGS="-march=native -Ofast -fgraphite-identity -floop-nest-optimize -fdevirtualize-at-ltrans -fipa-pta -fno-semantic-interposition -flto=16 -fuse-linker-plugin -falign-functions=32 -pipe"
GENTOO_MIRRORS="http://www.gtlib.gatech.edu/pub/gentoo rsync://rsync.gtlib.gatech.edu/gentoo https://gentoo.osuosl.org/ http://gentoo.osuosl.org/ http://gentoo.mirrors.pair.com/ https://mirrors.rit.edu/gentoo/ http://mirrors.rit.edu/gentoo/ ftp://mirrors.rit.edu/gentoo/ rsync://mirrors.rit.edu/gentoo/ http://gentoo.mirrors.tds.net/gentoo"
LANG="en_US.utf8"
LC_ALL="en_US.utf8"
LDFLAGS="-march=native -Ofast -fgraphite-identity -floop-nest-optimize -fdevirtualize-at-ltrans -fipa-pta -fno-semantic-interposition -flto=16 -fuse-linker-plugin -falign-functions=32 -pipe -Wl,-Ofast -Wl,--sort-common -Wl,--as-needed -fuse-linker-plugin"
MAKEOPTS="NATIVE_FULL_AOT=1 -j16 -l16"
PKGDIR="/var/cache/binpkgs"
PORTAGE_CONFIGROOT="/"
PORTAGE_RSYNC_OPTS="--recursive --links --safe-links --perms --times --omit-dir-times --compress --force --whole-file --delete --stats --human-readable --timeout=180 --exclude=/distfiles --exclude=/local --exclude=/packages --exclude=/.git"
PORTAGE_TMPDIR="/var/tmp"
RUSTFLAGS="-C target-cpu=skylake"
SHELL="/bin/zsh"
USE="X acl alsa amd64 bzip2 cli crypt cups dri fortran gdbm iconv ipv6 libglvnd libtirpc multilib ncurses nptl openmp pam pcre readline seccomp split-usr ssl truetype unicode vaapi xattr xinerama xvmc zlib" ABI_X86="64" ADA_TARGET="gnat_2020" APACHE2_MODULES="authn_core authz_core socache_shmcb unixd actions alias auth_basic authn_alias authn_anon authn_dbm authn_default authn_file authz_dbm authz_default authz_groupfile authz_host authz_owner authz_user autoindex cache cgi cgid dav dav_fs dav_lock deflate dir disk_cache env expires ext_filter file_cache filter headers include info log_config logio mem_cache mime mime_magic negotiation rewrite setenvif speling status unique_id userdir usertrack vhost_alias" CALLIGRA_FEATURES="karbon sheets words" COLLECTD_PLUGINS="df interface irq load memory rrdtool swap syslog" CPU_FLAGS_X86="mmx mmxext sse sse2" ELIBC="glibc" GPSD_PROTOCOLS="ashtech aivdm earthmate evermore fv18 garmin garmintxt gpsclock greis isync itrax mtk3301 nmea ntrip navcom oceanserver oldstyle oncore rtcm104v2 rtcm104v3 sirf skytraq superstar2 timing tsip tripmate tnt ublox ubx" GRUB_PLATFORMS="efi-64" INPUT_DEVICES="libinput" KERNEL="linux" LCD_DEVICES="bayrad cfontz cfontz633 glk hd44780 lb216 lcdm001 mtxorb ncurses text" LIBREOFFICE_EXTENSIONS="presenter-console presenter-minimizer" LUA_SINGLE_TARGET="lua5-1" LUA_TARGETS="lua5-1" OFFICE_IMPLEMENTATION="libreoffice" PHP_TARGETS="php7-4 php8-0" POSTGRES_TARGETS="postgres12 postgres13" PYTHON_SINGLE_TARGET="python3_9" PYTHON_TARGETS="python3_9" RUBY_TARGETS="ruby26 ruby27" USERLAND="GNU" VIDEO_CARDS="intel i965 iris" XTABLES_ADDONS="quota2 psd pknock lscan length2 ipv4options ipset ipp2p iface geoip fuzzy condition tee tarpit sysrq proto steal rawnat logmark ipmark dhcpmac delude chaos account"
Unset: ADDR2LINE, AR, ARFLAGS, AS, ASFLAGS, CC, CCLD, CONFIG_SHELL, CPP, CPPFLAGS, CTARGET, CXX, CXXFILT, ELFEDIT, EXTRA_ECONF, F77FLAGS, FC, GCOV, GPROF, INSTALL_MASK, LD, LEX, LFLAGS, LIBTOOL, LINGUAS, MAKE, MAKEFLAGS, NM, OBJCOPY, OBJDUMP, PORTAGE_BINHOST, PORTAGE_BUNZIP2_COMMAND, PORTAGE_COMPRESS, PORTAGE_COMPRESS_FLAGS, PORTAGE_RSYNC_EXTRA_OPTS, RANLIB, READELF, SIZE, STRINGS, STRIP, YACC, YFLAGS

@LemonBreezes LemonBreezes changed the title Coq fails to compile when Ocaml is built with Ofast Coq fails to compile when Ocaml is built with -Ofast May 8, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant