-> yaourt -S coq --noconfirm

==> Downloading coq PKGBUILD from AUR...
x .SRCINFO
x PKGBUILD
jdarch commented on 2016-01-23 18:46
Shouldn't camlp5 or camlp4 be a dependency?

zorun commented on 2016-01-23 19:00
Indeed, when updating to 8.5, I thought camlp4 was bundled with ocaml.  I have now added the missing dependency, thanks!

srl commented on 2016-01-26 17:08
A nice touch would be a .desktop file for coqide. There's one at [1], for instance.

[1] https://github.com/nana4gonta/gentoo-prefix-overlay/blob/master/sci-mathematics/coq/files/coqide.desktop

tomoki commented on 2016-02-06 07:53
Thank you for mentaining this package!

I got following error when I build this package:

---
OCAMLDEP  checker/analyze.ml
OCAMLBEST -o bin/ocamllibdep
/usr/bin/ld: /usr/lib/ocaml/libasmrun.a(startup.o): relocation R_X86_64_32 against `.rodata.str1.1' can not be used when making a shared object; recompile with -fPIC
/usr/lib/ocaml/libasmrun.a: error adding symbols: Bad value
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
make[1]: *** No rule to make target 'bin/ocamllibdep', needed by 'grammar/grammar.mllib.d'.  Stop.
---

Any ideas?

zorun commented on 2016-02-11 12:48
Hi tomoki,

I cannot reproduce this error.  A quick search dig out these seemingly related bug reports:

https://bugs.archlinux.org/task/42748
http://caml.inria.fr/mantis/view.php?id=6693
https://bugzilla.redhat.com/show_bug.cgi?id=1195025

Which version of ocaml are you using?  Is your system up-to-date?

Could you provide the output of the start of compilation?  It should look like this: http://paste.aliens-lyon.fr/u3v
Can you also provide the output of "pacman -Qs ocaml"?

coq 8.5-2  (2016-01-23 18:56)
( Unsupported package: Potentially dangerous ! )
==> coq dependencies:
- gtk2 (already installed)
- ocaml (already installed)
- camlp4 (already installed)
- gtksourceview2 (already installed)
- ocaml-findlib (already installed) [makedepend]
- lablgtk2 (already installed) [makedepend]


==> Continue building coq ? [Y/n]
==> -----------------------------
==>
==> Building and installing package
==> Making package: coq 8.5-2 (Fri Feb 12 20:18:48 JST 2016)
==> Checking runtime dependencies...
==> Checking buildtime dependencies...
==> Retrieving sources...
-> Downloading coq-8.5.tar.gz...
% Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
Dload  Upload   Total   Spent    Left  Speed
100   238  100   238    0     0    110      0  0:00:02  0:00:02 --:--:--   110
100 5221k  100 5221k    0     0   141k      0  0:00:36  0:00:36 --:--:--  200k
==> Validating source files with md5sums...
coq-8.5.tar.gz ... Passed
==> Validating source files with sha1sums...
coq-8.5.tar.gz ... Passed
==> Validating source files with sha256sums...
coq-8.5.tar.gz ... Passed
==> Extracting sources...
-> Extracting coq-8.5.tar.gz with bsdtar
==> Starting build()...
You have GNU Make 4.1. Good!
You have OCaml 4.02.3. Good!
You have native-code compilation. Good!
LablGtk2 found (via ocamlfind), with native threads:
=> native CoqIde will be built.


Coq VM bytecode link flags  : -dllib -lcoqrun -dllpath /usr/lib/coq
Other bytecode link flags   :
OS dependent libraries      : -cclib -lunix
OCaml version               : 4.02.3
OCaml binaries in           : /usr/bin
OCaml library in            : /usr/lib/ocaml
Camlp4 version              : 4.02.3
Camlp4 binaries in          : /usr/bin
Camlp4 library in           : +camlp4
Native dynamic link support : true
Lablgtk2 library in         : +lablgtk2
CoqIde                      : opt
Documentation               : None
Web browser                 : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
Coq web site                : http://coq.inria.fr/

Paths for true installation:
- the Coq binaries will be copied in /usr/bin
- the Coq library will be copied in /usr/lib/coq
- the Coqide configuration files will be copied in /etc/xdg/coq/
- the Coqide data files will be copied in /usr/share/coq
- the Coq man pages will be copied in /usr/share/man
- the Coq documentation will be copied in /usr/share/doc/coq
- the Coq Emacs mode will be copied in /usr/share/emacs/site-lisp
- the Coqdoc LaTeX files will be copied in /usr/share/emacs/site-lisp

If anything is wrong above, please restart './configure'.

*Warning* To compile the system for a new architecture
don't forget to do a 'make clean' before './configure'.
make --warn-undefined-variable --no-builtin-rules -f Makefile.build BUILDGRAMMAR=1 grammar/grammar.cma grammar/q_constr.cmo
make[1]: Entering directory '/tmp/yaourt-tmp-tomoki/aur-coq/src/coq-8.5'
OCAMLLEX  tools/coqdep_lexer.mll
406 states, 7873 transitions, table size 33928 bytes
3479 additional bytes used for bindings
OCAMLBEST -o bin/coqdep_boot
/usr/bin/ld: /usr/lib/ocaml/libasmrun.a(startup.o): relocation R_X86_64_32 against `.rodata.str1.1' can not be used when making a shared object; recompile with -fPIC
/usr/lib/ocaml/libasmrun.a: error adding symbols: Bad value
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
OCAMLLEX  ide/config_lexer.mll
30 states, 1657 transitions, table size 6808 bytes
6052 additional bytes used for bindings
CAMLP4DEPS grammar/argextend.ml4
CAMLP4DEPS grammar/tacextend.ml4
CAMLP4DEPS grammar/q_coqast.ml4
CAMLP4DEPS grammar/q_constr.ml4
CAMLP4DEPS grammar/q_util.ml4
CAMLP4DEPS grammar/vernacextend.ml4
CAMLP4DEPS ide/project_file.ml4
CAMLP4DEPS ide/coqide_main.ml4
CAMLP4DEPS parsing/compat.ml4
CAMLP4DEPS parsing/g_proofs.ml4
CAMLP4DEPS parsing/g_constr.ml4
CAMLP4DEPS parsing/pcoq.ml4
CAMLP4DEPS parsing/g_vernac.ml4
CAMLP4DEPS parsing/g_prim.ml4
CAMLP4DEPS parsing/g_tactic.ml4
CAMLP4DEPS parsing/g_ltac.ml4
CAMLP4DEPS parsing/lexer.ml4
"/usr/bin/ocamlc.opt" -rectypes  -w -3 -c -I "+camlp4" -pp '"/usr/bin/camlp4orf" -I "/usr/lib/ocaml" -I "/usr/lib/ocaml"/threads -I "+camlp4" unix.cma threads.cma -impl' -impl tools/compat5.mlp
"/usr/bin/ocamlc.opt" -rectypes  -w -3 -c -I "+camlp4" -pp '"/usr/bin/camlp4orf" -I "/usr/lib/ocaml" -I "/usr/lib/ocaml"/threads -I "+camlp4" unix.cma threads.cma -impl' -impl tools/compat5b.mlp
CAMLP4O   grammar/argextend.ml4
CAMLP4O   grammar/tacextend.ml4
CAMLP4O   grammar/q_coqast.ml4
CAMLP4O   grammar/q_constr.ml4
CAMLP4O   grammar/q_util.ml4
CAMLP4O   grammar/vernacextend.ml4
CAMLP4O   ide/project_file.ml4
CAMLP4O   ide/coqide_main.ml4
CAMLP4O   parsing/compat.ml4
CAMLP4O   parsing/g_proofs.ml4
CAMLP4O   parsing/g_constr.ml4
CAMLP4O   parsing/pcoq.ml4
CAMLP4O   parsing/g_vernac.ml4
CAMLP4O   parsing/g_prim.ml4
CAMLP4O   parsing/g_tactic.ml4
CAMLP4O   parsing/g_ltac.ml4
CAMLP4O   parsing/lexer.ml4
ECHO... > plugins/quote/quote_plugin_mod.ml
ECHO... > plugins/extraction/extraction_plugin_mod.ml
ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
ECHO... > plugins/btauto/btauto_plugin_mod.ml
ECHO... > plugins/micromega/micromega_plugin_mod.ml
ECHO... > plugins/romega/romega_plugin_mod.ml
ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
ECHO... > plugins/firstorder/ground_plugin_mod.ml
ECHO... > plugins/funind/recdef_plugin_mod.ml
ECHO... > plugins/fourier/fourier_plugin_mod.ml
ECHO... > plugins/cc/cc_plugin_mod.ml
ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
ECHO... > plugins/omega/omega_plugin_mod.ml
ECHO... > plugins/derive/derive_plugin_mod.ml
ECHO... > plugins/decl_mode/decl_mode_plugin_mod.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})
ECHO... > tools/tolink.ml
OCAMLLEX  lib/xml_lexer.mll
80 states, 774 transitions, table size 3576 bytes
OCAMLLEX  tools/gallina_lexer.mll
190 states, 498 transitions, table size 3132 bytes
OCAMLLEX  tools/coqdoc/cpretty.mll
2628 states, 8154 transitions, table size 48384 bytes
OCAMLLEX  tools/coqwc.mll
230 states, 784 transitions, table size 4516 bytes
OCAMLLEX  ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX  ide/coq_lex.mll
30 states, 505 transitions, table size 2200 bytes
OCAMLBEST -o bin/coqdep_boot
/usr/bin/ld: /usr/lib/ocaml/libasmrun.a(startup.o): relocation R_X86_64_32 against `.rodata.str1.1' can not be used when making a shared object; recompile with -fPIC
/usr/lib/ocaml/libasmrun.a: error adding symbols: Bad value
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
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})
make[1]: *** No rule to make target 'bin/coqdep_boot', needed by 'grammar/grammar.mllib.d'.  Stop.
make[1]: Leaving directory '/tmp/yaourt-tmp-tomoki/aur-coq/src/coq-8.5'
make: *** [submake] Error 2
Makefile:158: recipe for target 'submake' failed
==> ERROR: A failure occurred in build().
Aborting...
==> ERROR: Makepkg was unable to build coq.
==> Restart building coq ? [y/N]
==> ----------------------------
==>