Gentoo Forums
Gentoo Forums
Gentoo Forums
Quick Search: in
[solved] trouble emerging sci-mathematics/coq-8.3_p1
View unanswered posts
View posts from last 24 hours

Reply to topic    Gentoo Forums Forum Index Portage & Programming
View previous topic :: View next topic  
Author Message

Joined: 02 May 2006
Posts: 44
Location: nerd town

PostPosted: Mon Feb 11, 2013 2:48 am    Post subject: [solved] trouble emerging sci-mathematics/coq-8.3_p1 Reply with quote


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!


>>> 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                      :

  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/
sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' \
kernel/byterun/coq_instruct.h | \
awk -f kernel/make-opcodes > kernel/ \
|| ( RV=$?; rm -f "kernel/"; exit ${RV} )
"ocaml" theories/Numbers/Natural/BigN/ > theories/Numbers/Natural/BigN/NMake_gen.v
TOUCH     tools/
TOUCH     tools/
TOUCH     lib/
TOUCH     lib/


OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
OCAMLOPT  checker/
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/
OCAMLOPT  plugins/micromega/
OCAMLOPT -o plugins/micromega/csdpcert
true plugins/micromega/csdpcert
OCAMLC    ide/utils/okey.mli
OCAMLC    ide/utils/
File "ide/utils/", 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)
         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)
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'

Portage (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
CFLAGS="-march=core2 -mtune=core2 -O2 -pipe"
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"
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"
LDFLAGS="-Wl,-O1 -Wl,--as-needed"
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"
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"

exobrain saibot # emerge -pqv '=sci-mathematics/coq-8.3_p1'

[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
View user's profile Send private message

Joined: 09 Dec 2012
Posts: 70

PostPosted: Mon Feb 11, 2013 5:54 pm    Post subject: Reply with quote

Thanks for your inquiry. Can you please post the output of ide/utils/, preferably at someplace like with a link for us? Thanks!!
Back to top
View user's profile Send private message

Joined: 24 Nov 2010
Posts: 211
Location: AU

PostPosted: Tue Feb 12, 2013 9:58 am    Post subject: Reply with quote

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
View user's profile Send private message

Joined: 02 May 2006
Posts: 44
Location: nerd town

PostPosted: Thu Feb 14, 2013 1:46 pm    Post subject: Reply with quote

Thanks both for the replies!
My /var/tmp/portage/sci-mathematics/coq-8.3_p1/work/coq-8.3pl1/ide/utils

Unmasking coq-8.4_1 has worked! The ebuild has successfully emerged. Now theorem proving can begin 8)
Back to top
View user's profile Send private message
Display posts from previous:   
Reply to topic    Gentoo Forums Forum Index Portage & Programming All times are GMT
Page 1 of 1

Jump to:  
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