View previous topic :: View next topic |
Author |
Message |
saibot n00b
Joined: 02 May 2006 Posts: 44 Location: nerd town
|
Posted: Mon Feb 11, 2013 2:48 am Post subject: [solved] trouble emerging sci-mathematics/coq-8.3_p1 |
|
|
Hi,
after a long hiatus with gentoo, I'm back and very happy with my system which works super smoothly (thanks guys!). Now I'm having trouble installing a package; I hope that the information below is sufficient to get some help here.
Thanks in advance!
/var/tmp/portage/sci-mathematics/coq-8.3_p1/temp/build.log
Code: |
>>> Unpacking source...
>>> Unpacking coq-8.3pl1.tar.gz to /var/tmp/portage/sci-mathematics/coq-8.3_p1/work
>>> Source unpacked in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work
>>> Preparing source in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1 ...
>>> Source prepared.
>>> Configuring source in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1 ...
You have GNU Make >= 3.81. Good!
You have Objective-Caml 3.12.1. Good!
You have native-code compilation. Good!
LablGtk2 found, native threads: native CoqIde will be available.
Coq top directory : /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1
Architecture : x86_64
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath '/usr/lib64/coq'
Coq tools bytecode link flags :
OS dependent libraries : -cclib -lunix
Objective-Caml/Camlp4 version : 3.12.1
Objective-Caml/Camlp4 binaries in : /usr/bin
Objective-Caml library in : /usr/lib64/ocaml
Camlp4 library in : /usr/lib64/ocaml/camlp5
Native dynamic link support : true
Lablgtk2 library in : /usr/lib64/ocaml/lablgtk2
Documentation : None
CoqIde : opt
Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
Coq web site : http://coq.inria.fr/
Paths for true installation:
binaries will be copied in /usr/bin
library will be copied in /usr/lib64/coq
man pages will be copied in /usr/share/man
documentation will be copied in /usr/share/doc/coq-8.3_p1
emacs mode will be copied in /usr/share/emacs/site-lisp
If anything in the above is wrong, please restart './configure'.
*Warning* To compile the system for a new architecture
don't forget to do a 'make archclean' before './configure'.
>>> Source configured.
>>> Compiling source in /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1 ...
make -j5 STRIP=true -j1
*****************************************************
*****************************************************
****************** Entering stage1 ******************
*****************************************************
*****************************************************
make --warn-undefined-variable --no-builtin-rules -f Makefile.stage1 "stage1"
make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'
sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
-e '/^}/q' kernel/byterun/coq_instruct.h > \
kernel/byterun/coq_jumptbl.h \
|| ( RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV} )
CCDEP kernel/byterun/coq_fix_code.c
CCDEP kernel/byterun/coq_interp.c
CCDEP kernel/byterun/coq_values.c
CCDEP kernel/byterun/coq_memory.c
OCAMLLEX tools/coqdep_lexer.mll
200 states, 5470 transitions, table size 23080 bytes
2243 additional bytes used for bindings
OCAMLLEX tools/coqdoc/cpretty.mll
2130 states, 6466 transitions, table size 38644 bytes
OCAMLLEX tools/gallina_lexer.mll
190 states, 498 transitions, table size 3132 bytes
OCAMLLEX tools/coqwc.mll
230 states, 833 transitions, table size 4712 bytes
OCAMLLEX ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX ide/highlight.mll
455 states, 31494 transitions, table size 128706 bytes
OCAMLLEX ide/coq_lex.mll
457 states, 31161 transitions, table size 127386 bytes
OCAMLLEX ide/config_lexer.mll
13 states, 332 transitions, table size 1406 bytes
OCAMLLEX dev/ocamlweb-doc/lex.mll
99 states, 6415 transitions, table size 26254 bytes
OCAMLLEX plugins/dp/dp_zenon.mll
85 states, 637 transitions, table size 3058 bytes
1881 additional bytes used for bindings
OCAMLYACC ide/config_parser.mly
OCAMLYACC dev/ocamlweb-doc/syntax.mly
3 shift/reduce conflicts.
ECHO... > scripts/tolink.ml
sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \
kernel/byterun/coq_instruct.h | \
awk -f kernel/make-opcodes > kernel/copcodes.ml \
|| ( RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV} )
"ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > theories/Numbers/Natural/BigN/NMake_gen.v
TOUCH tools/coq_tex.ml
TOUCH tools/coq_makefile.ml
TOUCH lib/pp.ml
TOUCH lib/compat.ml
[...]
OCAMLOPT checker/type_errors.ml
OCAMLOPT checker/modops.ml
OCAMLOPT checker/inductive.ml
OCAMLOPT checker/typeops.ml
OCAMLOPT checker/indtypes.ml
OCAMLOPT checker/subtyping.ml
OCAMLOPT checker/mod_checking.ml
OCAMLOPT checker/safe_typing.ml
OCAMLOPT checker/check.ml
OCAMLOPT checker/check_stat.ml
OCAMLOPT checker/checker.ml
OCAMLOPT -a -o checker/check.cmxa
OCAMLOPT -o bin/coqchk.opt
true bin/coqchk.opt
cd bin && ln -sf coqchk.opt coqchk
OCAMLC plugins/micromega/sos.mli
OCAMLOPT plugins/micromega/sos.ml
OCAMLOPT plugins/micromega/csdpcert.ml
OCAMLOPT -o plugins/micromega/csdpcert
true plugins/micromega/csdpcert
OCAMLC ide/utils/okey.mli
OCAMLC ide/utils/okey.ml
File "ide/utils/okey.ml", line 102, characters 46-55:
Error: This expression has type Gdk.Tags.modifier list
but an expression was expected of type
([< `BUTTON1
| `BUTTON2
| `BUTTON3
| `BUTTON4
| `BUTTON5
| `CONTROL
| `LOCK
| `MOD1
| `MOD2
| `MOD3
| `MOD4
| `MOD5
| `SHIFT ]
as 'a)
list
Type
Gdk.Tags.modifier =
[ `BUTTON1
| `BUTTON2
| `BUTTON3
| `BUTTON4
| `BUTTON5
| `CONTROL
| `HYPER
| `LOCK
| `META
| `MOD1
| `MOD2
| `MOD3
| `MOD4
| `MOD5
| `RELEASE
| `SHIFT
| `SUPER ]
is not compatible with type 'a
The second variant type does not allow tag(s)
`HYPER, `META, `RELEASE, `SUPER
make[1]: *** [ide/utils/okey.cmo] Error 2
make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1'
make: *** [world] Error 2
emake failed
|
exobrain saibot # emerge --info '=sci-mathematics/coq-8.3_p1'
Code: |
Portage 2.1.11.31 (default/linux/amd64/10.0/desktop, gcc-4.6.3, glibc-2.15-r3, 3.6.11-gentoo x86_64)
=================================================================
System Settings
=================================================================
System uname: Linux-3.6.11-gentoo-x86_64-Intel-R-_Core-TM-_i7-2640M_CPU_@_2.80GHz-with-gentoo-2.1
Timestamp of tree: Tue, 05 Feb 2013 23:30:01 +0000
ld GNU ld (GNU Binutils) 2.22
app-shells/bash: 4.2_p37
dev-java/java-config: 2.1.12-r1
dev-lang/python: 2.7.3-r2, 3.2.3
dev-util/cmake: 2.8.9
dev-util/pkgconfig: 0.27.1
sys-apps/baselayout: 2.1-r1
sys-apps/openrc: 0.11.8
sys-apps/sandbox: 2.5
sys-devel/autoconf: 2.13, 2.69
sys-devel/automake: 1.11.6
sys-devel/binutils: 2.22-r1
sys-devel/gcc: 4.6.3
sys-devel/gcc-config: 1.7.3
sys-devel/libtool: 2.4-r1
sys-devel/make: 3.82-r4
sys-kernel/linux-headers: 3.6 (virtual/os-headers)
sys-libs/glibc: 2.15-r3
Repositories: gentoo
ACCEPT_KEYWORDS="amd64"
ACCEPT_LICENSE="* -@EULA"
CBUILD="x86_64-pc-linux-gnu"
CFLAGS="-march=core2 -mtune=core2 -O2 -pipe"
CHOST="x86_64-pc-linux-gnu"
CONFIG_PROTECT="/etc /usr/share/gnupg/qualified.txt /usr/share/openvpn/easy-rsa"
CONFIG_PROTECT_MASK="${EPREFIX}/etc/gconf /etc/ca-certificates.conf /etc/dconf /etc/env.d /etc/fonts/fonts.conf /etc/gconf /etc/gentoo-release /etc/revdep-rebuild /etc/sandbox.d /etc/terminfo /etc/texmf/language.dat.d /etc/texmf/language.def.d /etc/texmf/updmap.d /etc/texmf/web2c"
CXXFLAGS="-march=core2 -mtune=core2 -O2 -pipe"
DISTDIR="/usr/portage/distfiles"
FCFLAGS="-O2 -pipe"
FEATURES="assume-digests binpkg-logs config-protect-if-modified distlocks ebuild-locks fixlafiles merge-sync news parallel-fetch protect-owned sandbox sfperms strict unknown-features-warn unmerge-logs unmerge-orphans userfetch"
FFLAGS="-O2 -pipe"
GENTOO_MIRRORS="ftp://mirror.csclub.uwaterloo.ca/gentoo-distfiles/"
LANG="en_US.UTF-8"
LDFLAGS="-Wl,-O1 -Wl,--as-needed"
MAKEOPTS="-j5"
PKGDIR="/usr/portage/packages"
PORTAGE_CONFIGROOT="/"
PORTAGE_RSYNC_OPTS="--recursive --links --safe-links --perms --times --compress --force --whole-file --delete --stats --human-readable --timeout=180 --exclude=/distfiles --exclude=/local --exclude=/packages"
PORTAGE_TMPDIR="/var/tmp"
PORTDIR="/usr/portage"
PORTDIR_OVERLAY=""
SYNC="rsync://rsync.gentoo.org/gentoo-portage"
USE="X a52 aac acl acpi alsa amd64 ao bash-completion berkdb branding bzip2 cairo cdda cdr cjk cli consolekit cracklib crypt css cups cxx dbus djvu dri dts dvd dvdr emboss exif fam ffmpeg firefox flac fontconfig fortran ftp gdbm gif gimp gnome gnome-keyring gnuplot gphoto2 gpm gps gtk hal iconv imagemagick ipv6 javascript jpeg kpathsea lame latex lcms ldap libnotify mad mmx mng modules mozilla mp3 mp4 mpeg mudflap multilib musicbrainz ncurses networkmanager nls nptl nsplugin offensive ogg openal opengl openmp opus pam pango pcmcia pcre pdf php png policykit ppds pulseaudio python qt3support readline rss sdl session sound spell sqlite sse sse2 sse3 ssl startup-notification svg symlink tcpd tiff truetype udev udisks unicode upower usb v4l vim-syntax vorbis wifi wxwidgets x264 xcb xinerama xml xv xvid zlib zsh-completion" ABI_X86="64" ALSA_CARDS="ali5451 als4000 atiixp atiixp-modem bt87x ca0106 cmipci emu10k1x ens1370 ens1371 es1938 es1968 fm801 hda-intel intel8x0 intel8x0m maestro3 trident usb-audio via82xx via82xx-modem ymfpci" ALSA_PCM_PLUGINS="adpcm alaw asym copy dmix dshare dsnoop empty extplug file hooks iec958 ioplug ladspa lfloat linear meter mmap_emul mulaw multi null plug rate route share shm softvol" 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="kexi words flow plan sheets stage tables krita karbon braindump" CAMERAS="ptp2" COLLECTD_PLUGINS="df interface irq load memory rrdtool swap syslog" ELIBC="glibc" GPSD_PROTOCOLS="ashtech aivdm earthmate evermore fv18 garmin garmintxt gpsclock itrax mtk3301 nmea ntrip navcom oceanserver oldstyle oncore rtcm104v2 rtcm104v3 sirf superstar2 timing tsip tripmate tnt ubx" INPUT_DEVICES="keyboard mouse evdev synaptics" KERNEL="linux" LCD_DEVICES="bayrad cfontz cfontz633 glk hd44780 lb216 lcdm001 mtxorb ncurses text" LIBREOFFICE_EXTENSIONS="presenter-console presenter-minimizer" PHP_TARGETS="php5-3" PYTHON_SINGLE_TARGET="python2_7" PYTHON_TARGETS="python2_7 python3_2" RUBY_TARGETS="ruby18 ruby19" USERLAND="GNU" VIDEO_CARDS="fbdev glint intel mach64 mga nouveau nv r128 radeon savage sis tdfx trident vesa via vmware dummy v4l" XTABLES_ADDONS="quota2 psd pknock lscan length2 ipv4options ipset ipp2p iface geoip fuzzy condition tee tarpit sysrq steal rawnat logmark ipmark dhcpmac delude chaos account"
Unset: CPPFLAGS, CTARGET, EMERGE_DEFAULT_OPTS, INSTALL_MASK, LC_ALL, PORTAGE_BUNZIP2_COMMAND, PORTAGE_COMPRESS, PORTAGE_COMPRESS_FLAGS, PORTAGE_RSYNC_EXTRA_OPTS, USE_PYTHON
|
exobrain saibot # emerge -pqv '=sci-mathematics/coq-8.3_p1'
Code: |
[ebuild N ] sci-mathematics/coq-8.3_p1 USE="gtk ocamlopt -debug -doc"
|
Last edited by saibot on Thu Feb 14, 2013 1:46 pm; edited 1 time in total |
|
Back to top |
|
|
windex n00b
Joined: 09 Dec 2012 Posts: 70
|
Posted: Mon Feb 11, 2013 5:54 pm Post subject: |
|
|
Thanks for your inquiry. Can you please post the output of ide/utils/okey.ml, preferably at someplace like codepad.org with a link for us? Thanks!! |
|
Back to top |
|
|
gienah Developer
Joined: 24 Nov 2010 Posts: 212 Location: AU
|
Posted: Tue Feb 12, 2013 9:58 am Post subject: |
|
|
This could be fixed by choosing 1 (and only 1) of the following options:
(1) unmask sci-mathematics/coq-8.4_p1
exlusive or
(2) unmask sci-mathematics/coq-8.3_p4
exclusive or
(3) mask >=dev-ml/lablgtk-2.16
The problem is that dev-ml/lablgtk-2.16.0 has been stablized, but only coq-8.3_p4 and coq-8.4_p1 are patched
for dev-ml/lablgtk-2.16.0.
PS I know sci-mathematics/coq-8.4_p1 works as I use it. |
|
Back to top |
|
|
saibot n00b
Joined: 02 May 2006 Posts: 44 Location: nerd town
|
|
Back to top |
|
|
|
|
You cannot post new topics in this forum You cannot reply to topics in this forum You cannot edit your posts in this forum You cannot delete your posts in this forum You cannot vote in polls in this forum
|
|