damien-pous / relation-algebra Goto Github PK

View Code? Open in Web Editor NEW

43.0 43.0 15.0 555 KB

Relation algebra library for Coq

License: GNU Lesser General Public License v3.0

Makefile 0.28% Coq 84.44% HTML 3.39% OCaml 11.89%

relation-algebra's People

Contributors

Stargazers

Watchers

Forkers

chdoc sr-lab skyskimmer ppedrot ejgallego simonboulier herbelin eupp mrhaandi jfehrle gares mattam82 czhang03 proux01

relation-algebra's Issues

dev version of relation-algebra compatible with coq.dev

Since relation-algebra is in Coq's CI, would you mind including a dev version tracking its master branch to coq-extra-dev opam repo? This would make it easier to include relation-algebra as a dependency into a CI for projects aiming to stay compatible with Coq's dev version and relying on relation-algebra package.

By the way, I'm happy to give you a hand with this if you think this is something worth doing. Thank you in advance!

Coq 8.14 compatibility release?

Hi, looks like the deps have Coq 8.14 support. Are there any plans to make a Coq 8.14 compatibility release? Thanks in advance!

Inclusion into the Coq Platform

Dear realtion-algebra Team,

a user of your development requested here: (coq/platform#167) to include your development into the Coq Platform, which is the standard user facing distribution of Coq.

Coq Platform has a "full" and "extended" level. Inclusion in the "full" level requires an explicit statement by the maintainers, that they agree to the charter of the Coq Platform and intend to publish compatible releases for each release of Coq in a reasonable time frame. For the "extended" level the rules are more relaxed. For developments in the "full" level, users should be able to rely on that the package is maintained, so that they can base their own development on it without a large risk that they have to factor it out again later cause of maintenance issues.

Can you please comment in the Coq Platform issue mentioned above if you do want your package included in the Coq Platform in agreement to the Coq Platform charter, and if so which level you would prefer?

Best regards,

Michael

Compilation error with Coq 8.5.1

Hi,

The versions 1.4 and 1.5 of relation-algebra do not compile with Coq 8.5.1. For example, on a six cores machine, the command:

opam list; opam install -y -v coq-relation-algebra.1.5

outputs:

# Installed packages for system:
base-bigarray   base  Bigarray library distributed with the OCaml compiler
base-threads    base  Threads library distributed with the OCaml compiler
base-unix       base  Unix library distributed with the OCaml compiler
camlp5          6.14  Preprocessor-pretty-printer of OCaml
coq            8.5.1  Formal proof management system.
The following actions will be performed:
  - install coq-relation-algebra 1.5
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-relation-algebra: http] Command started
[coq-relation-algebra: http] Command started
[coq-relation-algebra.1.5] https://github.com/damien-pous/relation-algebra/archive/v1.5.tar.gz downloaded
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-relation-algebra: coq_makefile Make] Command started
+ coq_makefile "-f" "Make" "-o" "Makefile" (CWD=/home/bench/.opam/system/build/coq-relation-algebra.1.5)
[coq-relation-algebra: make] Command started
+ make "-j6" (CWD=/home/bench/.opam/system/build/coq-relation-algebra.1.5)
- /usr/local/bin/ocamldep.opt -slash -I "." "kat_dec.mli" > "kat_dec.mli.d" || ( RV=$?; rm -f "kat_dec.mli.d"; exit ${RV} )
- "coqdep" -c -I "." -c "kat_reification.mllib" > "kat_reification.mllib.d" || ( RV=$?; rm -f "kat_reification.mllib.d"; exit ${RV} )
- /usr/local/bin/ocamldep.opt -slash -I "." "kat_dec.ml" > "kat_dec.ml.d" || ( RV=$?; rm -f "kat_dec.ml.d"; exit ${RV} )
- /usr/local/bin/ocamldep.opt -slash -I "." "ra_common.ml" > "ra_common.ml.d" || ( RV=$?; rm -f "ra_common.ml.d"; exit ${RV} )
- /usr/local/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "kat_reification.ml4" > "kat_reification.ml4.d" || ( RV=$?; rm -f "kat_reification.ml4.d"; exit ${RV} )
- /usr/local/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_reification.ml4" > "ra_reification.ml4.d" || ( RV=$?; rm -f "ra_reification.ml4.d"; exit ${RV} )
- /usr/local/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "mrewrite.ml4" > "mrewrite.ml4.d" || ( RV=$?; rm -f "mrewrite.ml4.d"; exit ${RV} )
- /usr/local/bin/ocamldep.opt -slash -I "." -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_fold.ml4" > "ra_fold.ml4.d" || ( RV=$?; rm -f "ra_fold.ml4.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "paterson.v" > "paterson.v.d" || ( RV=$?; rm -f "paterson.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "imp.v" > "imp.v.d" || ( RV=$?; rm -f "imp.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "compiler_opts.v" > "compiler_opts.v.d" || ( RV=$?; rm -f "compiler_opts.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "relalg.v" > "relalg.v.d" || ( RV=$?; rm -f "relalg.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "kat_tac.v" > "kat_tac.v.d" || ( RV=$?; rm -f "kat_tac.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "kat_reification.v" > "kat_reification.v.d" || ( RV=$?; rm -f "kat_reification.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "kat_untyping.v" > "kat_untyping.v.d" || ( RV=$?; rm -f "kat_untyping.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "ugregex_dec.v" > "ugregex_dec.v.d" || ( RV=$?; rm -f "ugregex_dec.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "ugregex.v" > "ugregex.v.d" || ( RV=$?; rm -f "ugregex.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "kat_completeness.v" > "kat_completeness.v.d" || ( RV=$?; rm -f "kat_completeness.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "gregex.v" > "gregex.v.d" || ( RV=$?; rm -f "gregex.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "glang.v" > "glang.v.d" || ( RV=$?; rm -f "glang.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "traces.v" > "traces.v.d" || ( RV=$?; rm -f "traces.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "atoms.v" > "atoms.v.d" || ( RV=$?; rm -f "atoms.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "ka_completeness.v" > "ka_completeness.v.d" || ( RV=$?; rm -f "ka_completeness.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "nfa.v" > "nfa.v.d" || ( RV=$?; rm -f "nfa.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "dfa.v" > "dfa.v.d" || ( RV=$?; rm -f "dfa.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "bmx.v" > "bmx.v.d" || ( RV=$?; rm -f "bmx.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "rmx.v" > "rmx.v.d" || ( RV=$?; rm -f "rmx.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "regex.v" > "regex.v.d" || ( RV=$?; rm -f "regex.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "untyping.v" > "untyping.v.d" || ( RV=$?; rm -f "untyping.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "matrix_ext.v" > "matrix_ext.v.d" || ( RV=$?; rm -f "matrix_ext.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "matrix.v" > "matrix.v.d" || ( RV=$?; rm -f "matrix.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "sums.v" > "sums.v.d" || ( RV=$?; rm -f "sums.v.d"; exit ${RV} )
- *** Warning: kat_reification.mllib already found in . (discarding ./kat_reification.mllib)
- "coqdep" -c -R "." RelationAlgebra -I "." "sups.v" > "sups.v.d" || ( RV=$?; rm -f "sups.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "lset.v" > "lset.v.d" || ( RV=$?; rm -f "lset.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "lang.v" > "lang.v.d" || ( RV=$?; rm -f "lang.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "rel.v" > "rel.v.d" || ( RV=$?; rm -f "rel.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "boolean.v" > "boolean.v.d" || ( RV=$?; rm -f "boolean.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "prop.v" > "prop.v.d" || ( RV=$?; rm -f "prop.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "normalisation.v" > "normalisation.v.d" || ( RV=$?; rm -f "normalisation.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "syntax.v" > "syntax.v.d" || ( RV=$?; rm -f "syntax.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "lsyntax.v" > "lsyntax.v.d" || ( RV=$?; rm -f "lsyntax.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "move.v" > "move.v.d" || ( RV=$?; rm -f "move.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "rewriting.v" > "rewriting.v.d" || ( RV=$?; rm -f "rewriting.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "kat.v" > "kat.v.d" || ( RV=$?; rm -f "kat.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "factors.v" > "factors.v.d" || ( RV=$?; rm -f "factors.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "kleene.v" > "kleene.v.d" || ( RV=$?; rm -f "kleene.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "monoid.v" > "monoid.v.d" || ( RV=$?; rm -f "monoid.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "lattice.v" > "lattice.v.d" || ( RV=$?; rm -f "lattice.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "level.v" > "level.v.d" || ( RV=$?; rm -f "level.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "powerfix.v" > "powerfix.v.d" || ( RV=$?; rm -f "powerfix.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "pair.v" > "pair.v.d" || ( RV=$?; rm -f "pair.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "denum.v" > "denum.v.d" || ( RV=$?; rm -f "denum.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "ordinal.v" > "ordinal.v.d" || ( RV=$?; rm -f "ordinal.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "positives.v" > "positives.v.d" || ( RV=$?; rm -f "positives.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "comparisons.v" > "comparisons.v.d" || ( RV=$?; rm -f "comparisons.v.d"; exit ${RV} )
- "coqdep" -c -R "." RelationAlgebra -I "." "common.v" > "common.v.d" || ( RV=$?; rm -f "common.v.d"; exit ${RV} )
- "coqc"  -q  -R "." RelationAlgebra -I "."   common
- "coqc"  -q  -R "." RelationAlgebra -I "."   comparisons
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 ra_common.ml
- /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 ra_common.ml
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 kat_dec.mli
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 kat_dec.ml
- /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 kat_dec.ml
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl ra_fold.ml4
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl mrewrite.ml4
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl ra_reification.ml4
- /usr/local/bin/ocamlc.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl kat_reification.ml4
- /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl kat_reification.ml4
- "coqc"  -q  -R "." RelationAlgebra -I "."   powerfix
- "coqc"  -q  -R "." RelationAlgebra -I "."   level
- /usr/local/bin/ocamlopt.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -shared -o ra_common.cmxs ra_common.cmx
- /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl ra_fold.ml4
- /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl mrewrite.ml4
- /usr/local/bin/ocamlopt.opt -c -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -pp '/home/bench/.opam/system/bin/camlp5o -I /usr/local/lib/ocaml/ -I /usr/local/lib/ocaml/threads/ -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl ra_reification.ml4
- /usr/local/bin/ocamlc.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -a -o kat_reification.cma kat_dec.cmo kat_reification.cmo
- /usr/local/bin/ocamlopt.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -a -o kat_reification.cmxa kat_dec.cmx kat_reification.cmx
- /usr/local/bin/ocamlopt.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -linkall -shared -o kat_reification.cmxs kat_reification.cmxa
- /usr/local/bin/ocamlopt.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -shared -o mrewrite.cmxs mrewrite.cmx
- /usr/local/bin/ocamlopt.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -shared -o ra_reification.cmxs ra_reification.cmx
- "coqc"  -q  -R "." RelationAlgebra -I "."   positives
- "coqc"  -q  -R "." RelationAlgebra -I "."   ordinal
- /usr/local/bin/ocamlopt.opt -rectypes -thread  -I "." -I "/home/bench/.opam/system/lib/coq/kernel" -I "/home/bench/.opam/system/lib/coq/lib" -I "/home/bench/.opam/system/lib/coq/library" -I "/home/bench/.opam/system/lib/coq/parsing" -I "/home/bench/.opam/system/lib/coq/pretyping" -I "/home/bench/.opam/system/lib/coq/interp" -I "/home/bench/.opam/system/lib/coq/printing" -I "/home/bench/.opam/system/lib/coq/intf" -I "/home/bench/.opam/system/lib/coq/proofs" -I "/home/bench/.opam/system/lib/coq/tactics" -I "/home/bench/.opam/system/lib/coq/tools" -I "/home/bench/.opam/system/lib/coq/toplevel" -I "/home/bench/.opam/system/lib/coq/stm" -I "/home/bench/.opam/system/lib/coq/grammar" -I "/home/bench/.opam/system/lib/coq/config" -I "/home/bench/.opam/system/lib/coq//plugins/btauto" -I "/home/bench/.opam/system/lib/coq//plugins/cc" -I "/home/bench/.opam/system/lib/coq//plugins/decl_mode" -I "/home/bench/.opam/system/lib/coq//plugins/derive" -I "/home/bench/.opam/system/lib/coq//plugins/extraction" -I "/home/bench/.opam/system/lib/coq//plugins/firstorder" -I "/home/bench/.opam/system/lib/coq//plugins/fourier" -I "/home/bench/.opam/system/lib/coq//plugins/funind" -I "/home/bench/.opam/system/lib/coq//plugins/micromega" -I "/home/bench/.opam/system/lib/coq//plugins/nsatz" -I "/home/bench/.opam/system/lib/coq//plugins/omega" -I "/home/bench/.opam/system/lib/coq//plugins/quote" -I "/home/bench/.opam/system/lib/coq//plugins/romega" -I "/home/bench/.opam/system/lib/coq//plugins/rtauto" -I "/home/bench/.opam/system/lib/coq//plugins/setoid_ring" -I "/home/bench/.opam/system/lib/coq//plugins/syntax" -I "/home/bench/.opam/system/lib/coq//plugins/xml" -I /home/bench/.opam/system/lib/camlp5 -shared -o ra_fold.cmxs ra_fold.cmx
- "coqc"  -q  -R "." RelationAlgebra -I "."   lattice
- "coqc"  -q  -R "." RelationAlgebra -I "."   denum
- "coqc"  -q  -R "." RelationAlgebra -I "."   pair
- "coqc"  -q  -R "." RelationAlgebra -I "."   monoid
- "coqc"  -q  -R "." RelationAlgebra -I "."   prop
- "coqc"  -q  -R "." RelationAlgebra -I "."   lset
- "coqc"  -q  -R "." RelationAlgebra -I "."   sups
- "coqc"  -q  -R "." RelationAlgebra -I "."   lsyntax
- "coqc"  -q  -R "." RelationAlgebra -I "."   kleene
- "coqc"  -q  -R "." RelationAlgebra -I "."   rewriting
- "coqc"  -q  -R "." RelationAlgebra -I "."   syntax
- "coqc"  -q  -R "." RelationAlgebra -I "."   boolean
- "coqc"  -q  -R "." RelationAlgebra -I "."   sums
- "coqc"  -q  -R "." RelationAlgebra -I "."   traces
- "coqc"  -q  -R "." RelationAlgebra -I "."   lang
- "coqc"  -q  -R "." RelationAlgebra -I "."   atoms
- "coqc"  -q  -R "." RelationAlgebra -I "."   factors
- "coqc"  -q  -R "." RelationAlgebra -I "."   kat
- "coqc"  -q  -R "." RelationAlgebra -I "."   glang
- "coqc"  -q  -R "." RelationAlgebra -I "."   rel
- "coqc"  -q  -R "." RelationAlgebra -I "."   ugregex
- "coqc"  -q  -R "." RelationAlgebra -I "."   ugregex_dec
- File "./ugregex_dec.v", line 104, characters 20-21:
- Error:
- In environment
- Pred : nat
- vars : forall e : ugregex, ?T
- e : ugregex
- i : Sigma
- The term "i" has type "Sigma" while it is expected to have type
-  "car (tst ?n)".
- Makefile:486: recipe for target 'ugregex_dec.vo' failed
- make: *** [ugregex_dec.vo] Error 1
- make: *** Waiting for unfinished jobs....
[ERROR] The compilation of coq-relation-algebra failed at "make -j6".
[coq-relation-algebra: rm] Command started
+ rm "-R" "/home/bench/.opam/system/lib/coq/user-contrib/RelationAlgebra" (CWD=/home/bench/.opam/system/build/coq-relation-algebra.1.5)
- rm: cannot remove '/home/bench/.opam/system/lib/coq/user-contrib/RelationAlgebra': No such file or directory
#=== ERROR while installing coq-relation-algebra.1.5 ==========================#
# opam-version         1.2.2
# os                   linux
# command              make -j6
# path                 /home/bench/.opam/system/build/coq-relation-algebra.1.5
# compiler             system (4.02.3)
# exit-code            2
# env-file             /home/bench/.opam/system/build/coq-relation-algebra.1.5/coq-relation-algebra-380-c61e7b.env
# stdout-file          /home/bench/.opam/system/build/coq-relation-algebra.1.5/coq-relation-algebra-380-c61e7b.out
# stderr-file          /home/bench/.opam/system/build/coq-relation-algebra.1.5/coq-relation-algebra-380-c61e7b.err
### stdout ###
# [...]
# "coqc"  -q  -R "." RelationAlgebra -I "."   traces
# "coqc"  -q  -R "." RelationAlgebra -I "."   lang
# "coqc"  -q  -R "." RelationAlgebra -I "."   atoms
# "coqc"  -q  -R "." RelationAlgebra -I "."   factors
# "coqc"  -q  -R "." RelationAlgebra -I "."   kat
# "coqc"  -q  -R "." RelationAlgebra -I "."   glang
# "coqc"  -q  -R "." RelationAlgebra -I "."   rel
# "coqc"  -q  -R "." RelationAlgebra -I "."   ugregex
# "coqc"  -q  -R "." RelationAlgebra -I "."   ugregex_dec
# Makefile:486: recipe for target 'ugregex_dec.vo' failed
### stderr ###
# [...]
# Error:
# In environment
# Pred : nat
# vars : forall e : ugregex, ?T
# e : ugregex
# i : Sigma
# The term "i" has type "Sigma" while it is expected to have type
#  "car (tst ?n)".
# make: *** [ugregex_dec.vo] Error 1
# make: *** Waiting for unfinished jobs....
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install coq-relation-algebra 1.5
No changes have been performed
'opam install -y -v coq-relation-algebra.1.5' failed.

As a result I corrected the OPAM packages: coq/opam@cc04f03

Coq 8.12 release?

Looks like neither v1.7.3 tag, nor the current master branch are compatible with Coq 8.12.

Please create a tag for Coq 8.18 in Coq Platform 2023.10

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.7.9) does not work with Coq 8.18.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 1c37f34 on repository https://github.com/damien-pous/relation-algebra - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.18, preferably before October 31st, 2023?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before October 31st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.18.0.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372

Coq 8.13 release?

Hi, the optional deps have recently gained support for Coq 8.13 (e.g. for aac-tactics -- coq/opam#1526) and the current master branch seems to compile fine with Coq 8.13 too. It would be great to have a new release! Thanks in advance.

Please create a tag for Coq 8.16 in Coq Platform 2022.09

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (preview) does not work with Coq 8.16+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 00f84a0 on repository https://github.com/damien-pous/relation-algebra - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.16, preferably before August 31, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before August 17, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.16+rc1.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#274

Licensing needs rework

README.md says to have a look at the LICENSE and COPYING files. The first is LGPL-3+ and the second is GPL-3.

There's also a COPYING.LESSER which is LGPL-3. The opam file also says LGPL-3+.

Oh, and the homepage says LGPL-3.

That makes three different licenses... could you clarify the situation?

I would like to package coq-relation-algebra for Debian, but my package won't fly if there's a licensing conendrum.

Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.19.0.

Coq Platform CI is currently testing opam package coq-relation-algebra.1.7.10
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.10/opam. This means we had to weaken some version restrictions in the opam package, but no other changes were required.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2024.01, please inform us as soon as possible and before March 31st, 2024!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

Please create a tag for Coq 8.17 in Coq Platform 2023.03

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.7.8) does not work with Coq 8.17+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit 649a442 on repository https://github.com/damien-pous/relation-algebra - which likely means that this commit does work in Coq CI.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.17, preferably before March 21st, 2023?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before March 21st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.17+rc1.

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

Compilation error using Coq 8.6

Hi, I tried to compile the library with Coq 8.6 and get the following error message:

slash -I "." "kat_dec.mli" > "kat_dec.mli.d" || ( RV=$?; rm -f "kat_dec.mli.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:386: recipe for target 'kat_dec.mli.d' failed
make: [kat_dec.mli.d] Error 127 (ignored)
"coqdep" -c -I "." "kat_reification.mllib" > "kat_reification.mllib.d" || ( RV=$?; rm -f "kat_reification.mllib.d"; exit ${RV} )
*** Warning: kat_reification.mllib already found in . (discarding ./kat_reification.mllib)
slash -I "." "ra_common.ml" > "ra_common.ml.d" || ( RV=$?; rm -f "ra_common.ml.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:404: recipe for target 'ra_common.ml.d' failed
make: [ra_common.ml.d] Error 127 (ignored)
slash -I "." "kat_dec.ml" > "kat_dec.ml.d" || ( RV=$?; rm -f "kat_dec.ml.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:404: recipe for target 'kat_dec.ml.d' failed
make: [kat_dec.ml.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_fold.ml4" > "ra_fold.ml4.d" || ( RV=$?; rm -f "ra_fold.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'ra_fold.ml4.d' failed
make: [ra_fold.ml4.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "mrewrite.ml4" > "mrewrite.ml4.d" || ( RV=$?; rm -f "mrewrite.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'mrewrite.ml4.d' failed
make: [mrewrite.ml4.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_reification.ml4" > "ra_reification.ml4.d" || ( RV=$?; rm -f "ra_reification.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'ra_reification.ml4.d' failed
make: [ra_reification.ml4.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "kat_reification.ml4" > "kat_reification.ml4.d" || ( RV=$?; rm -f "kat_reification.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'kat_reification.ml4.d' failed
make: [kat_reification.ml4.d] Error 127 (ignored)
"coqdep" -c -R "." RelationAlgebra -I "." "common.v" > "common.v.d" || ( RV=$?; rm -f "common.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "comparisons.v" > "comparisons.v.d" || ( RV=$?; rm -f "comparisons.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "positives.v" > "positives.v.d" || ( RV=$?; rm -f "positives.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "ordinal.v" > "ordinal.v.d" || ( RV=$?; rm -f "ordinal.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "denum.v" > "denum.v.d" || ( RV=$?; rm -f "denum.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "pair.v" > "pair.v.d" || ( RV=$?; rm -f "pair.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "powerfix.v" > "powerfix.v.d" || ( RV=$?; rm -f "powerfix.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "level.v" > "level.v.d" || ( RV=$?; rm -f "level.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "lattice.v" > "lattice.v.d" || ( RV=$?; rm -f "lattice.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "monoid.v" > "monoid.v.d" || ( RV=$?; rm -f "monoid.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "kleene.v" > "kleene.v.d" || ( RV=$?; rm -f "kleene.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "factors.v" > "factors.v.d" || ( RV=$?; rm -f "factors.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "kat.v" > "kat.v.d" || ( RV=$?; rm -f "kat.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "rewriting.v" > "rewriting.v.d" || ( RV=$?; rm -f "rewriting.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "move.v" > "move.v.d" || ( RV=$?; rm -f "move.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "lsyntax.v" > "lsyntax.v.d" || ( RV=$?; rm -f "lsyntax.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "syntax.v" > "syntax.v.d" || ( RV=$?; rm -f "syntax.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "normalisation.v" > "normalisation.v.d" || ( RV=$?; rm -f "normalisation.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "prop.v" > "prop.v.d" || ( RV=$?; rm -f "prop.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "boolean.v" > "boolean.v.d" || ( RV=$?; rm -f "boolean.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "rel.v" > "rel.v.d" || ( RV=$?; rm -f "rel.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "lang.v" > "lang.v.d" || ( RV=$?; rm -f "lang.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "lset.v" > "lset.v.d" || ( RV=$?; rm -f "lset.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "sups.v" > "sups.v.d" || ( RV=$?; rm -f "sups.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "sums.v" > "sums.v.d" || ( RV=$?; rm -f "sums.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "matrix.v" > "matrix.v.d" || ( RV=$?; rm -f "matrix.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "matrix_ext.v" > "matrix_ext.v.d" || ( RV=$?; rm -f "matrix_ext.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "untyping.v" > "untyping.v.d" || ( RV=$?; rm -f "untyping.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "regex.v" > "regex.v.d" || ( RV=$?; rm -f "regex.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "rmx.v" > "rmx.v.d" || ( RV=$?; rm -f "rmx.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "bmx.v" > "bmx.v.d" || ( RV=$?; rm -f "bmx.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "dfa.v" > "dfa.v.d" || ( RV=$?; rm -f "dfa.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "nfa.v" > "nfa.v.d" || ( RV=$?; rm -f "nfa.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "ka_completeness.v" > "ka_completeness.v.d" || ( RV=$?; rm -f "ka_completeness.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "atoms.v" > "atoms.v.d" || ( RV=$?; rm -f "atoms.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "traces.v" > "traces.v.d" || ( RV=$?; rm -f "traces.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "glang.v" > "glang.v.d" || ( RV=$?; rm -f "glang.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "gregex.v" > "gregex.v.d" || ( RV=$?; rm -f "gregex.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "kat_completeness.v" > "kat_completeness.v.d" || ( RV=$?; rm -f "kat_completeness.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "ugregex.v" > "ugregex.v.d" || ( RV=$?; rm -f "ugregex.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "ugregex_dec.v" > "ugregex_dec.v.d" || ( RV=$?; rm -f "ugregex_dec.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "kat_untyping.v" > "kat_untyping.v.d" || ( RV=$?; rm -f "kat_untyping.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "kat_reification.v" > "kat_reification.v.d" || ( RV=$?; rm -f "kat_reification.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "kat_tac.v" > "kat_tac.v.d" || ( RV=$?; rm -f "kat_tac.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "relalg.v" > "relalg.v.d" || ( RV=$?; rm -f "relalg.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "compiler_opts.v" > "compiler_opts.v.d" || ( RV=$?; rm -f "compiler_opts.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "imp.v" > "imp.v.d" || ( RV=$?; rm -f "imp.v.d"; exit ${RV} )
"coqdep" -c -R "." RelationAlgebra -I "." "paterson.v" > "paterson.v.d" || ( RV=$?; rm -f "paterson.v.d"; exit ${RV} )
slash -I "." "kat_dec.mli" > "kat_dec.mli.d" || ( RV=$?; rm -f "kat_dec.mli.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:386: recipe for target 'kat_dec.mli.d' failed
make: [kat_dec.mli.d] Error 127 (ignored)
slash -I "." "ra_common.ml" > "ra_common.ml.d" || ( RV=$?; rm -f "ra_common.ml.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:404: recipe for target 'ra_common.ml.d' failed
make: [ra_common.ml.d] Error 127 (ignored)
slash -I "." "kat_dec.ml" > "kat_dec.ml.d" || ( RV=$?; rm -f "kat_dec.ml.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:404: recipe for target 'kat_dec.ml.d' failed
make: [kat_dec.ml.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_fold.ml4" > "ra_fold.ml4.d" || ( RV=$?; rm -f "ra_fold.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'ra_fold.ml4.d' failed
make: [ra_fold.ml4.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "mrewrite.ml4" > "mrewrite.ml4.d" || ( RV=$?; rm -f "mrewrite.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'mrewrite.ml4.d' failed
make: [mrewrite.ml4.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "ra_reification.ml4" > "ra_reification.ml4.d" || ( RV=$?; rm -f "ra_reification.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'ra_reification.ml4.d' failed
make: [ra_reification.ml4.d] Error 127 (ignored)
slash -I "." -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "kat_reification.ml4" > "kat_reification.ml4.d" || ( RV=$?; rm -f "kat_reification.ml4.d"; exit ${RV} )
/bin/sh: 1: slash: not found
Makefile:395: recipe for target 'kat_reification.ml4.d' failed
make: [kat_reification.ml4.d] Error 127 (ignored)
"coqc" -q -R "." RelationAlgebra -I "." common
"coqc" -q -R "." RelationAlgebra -I "." level
"coqc" -q -R "." RelationAlgebra -I "." lattice
File "./lattice.v", line 46, characters 0-25:
Warning: Implicit Arguments is deprecated; use Arguments instead
[deprecated-implicit-arguments,deprecated]
c -rectypes -thread -I "." -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 ra_common.ml
/bin/sh: 1: c: not found
Makefile:398: recipe for target 'ra_common.cmo' failed
make: [ra_common.cmo] Error 127 (ignored)
c -rectypes -thread -I "." -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 ra_common.ml
/bin/sh: 1: c: not found
Makefile:401: recipe for target 'ra_common.cmx' failed
make: [ra_common.cmx] Error 127 (ignored)
rectypes -thread -I "." -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 -shared -o ra_common.cmxs ra_common.cmx
/bin/sh: 1: rectypes: not found
Makefile:407: recipe for target 'ra_common.cmxs' failed
make: [ra_common.cmxs] Error 127 (ignored)
c -rectypes -thread -I "." -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl ra_fold.ml4
/bin/sh: 1: c: not found
Makefile:389: recipe for target 'ra_fold.cmo' failed
make: [ra_fold.cmo] Error 127 (ignored)
c -rectypes -thread -I "." -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 -pp '/usr/bin/camlp5o -I -I threads/ -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl ra_fold.ml4
/bin/sh: 1: c: not found
Makefile:392: recipe for target 'ra_fold.cmx' failed
make: [ra_fold.cmx] Error 127 (ignored)
rectypes -thread -I "." -I "/usr/local/lib/coq/kernel" -I "/usr/local/lib/coq/lib" -I "/usr/local/lib/coq/library" -I "/usr/local/lib/coq/parsing" -I "/usr/local/lib/coq/pretyping" -I "/usr/local/lib/coq/interp" -I "/usr/local/lib/coq/printing" -I "/usr/local/lib/coq/intf" -I "/usr/local/lib/coq/proofs" -I "/usr/local/lib/coq/tactics" -I "/usr/local/lib/coq/tools" -I "/usr/local/lib/coq/toplevel" -I "/usr/local/lib/coq/stm" -I "/usr/local/lib/coq/grammar" -I "/usr/local/lib/coq/config" -I "/usr/local/lib/coq//plugins/btauto" -I "/usr/local/lib/coq//plugins/cc" -I "/usr/local/lib/coq//plugins/decl_mode" -I "/usr/local/lib/coq//plugins/derive" -I "/usr/local/lib/coq//plugins/extraction" -I "/usr/local/lib/coq//plugins/firstorder" -I "/usr/local/lib/coq//plugins/fourier" -I "/usr/local/lib/coq//plugins/funind" -I "/usr/local/lib/coq//plugins/micromega" -I "/usr/local/lib/coq//plugins/nsatz" -I "/usr/local/lib/coq//plugins/omega" -I "/usr/local/lib/coq//plugins/quote" -I "/usr/local/lib/coq//plugins/romega" -I "/usr/local/lib/coq//plugins/rtauto" -I "/usr/local/lib/coq//plugins/setoid_ring" -I "/usr/local/lib/coq//plugins/syntax" -I "/usr/local/lib/coq//plugins/xml" -I /usr/lib/ocaml/camlp5 -shared -o ra_fold.cmxs ra_fold.cmx
/bin/sh: 1: rectypes: not found
Makefile:407: recipe for target 'ra_fold.cmxs' failed
make: [ra_fold.cmxs] Error 127 (ignored)
"coqc" -q -R "." RelationAlgebra -I "." monoid
File "./monoid.v", line 39, characters 0-24:
Warning: Implicit Arguments is deprecated; use Arguments instead
[deprecated-implicit-arguments,deprecated]
File "./monoid.v", line 510, characters 0-30:
Warning: ofbool does not respect the uniform inheritance condition
[uniform-inheritance,typechecker]
File "./monoid.v", line 514, characters 0-30:
Error:
File not found on loadpath : ra_common.cmxs
Loadpath: /home/haozewu/Downloads/relation-algebra-1.6:/usr/local/lib/coq/plugins/setoid_ring:/usr/local/lib/coq/plugins/derive:/usr/local/lib/coq/plugins/firstorder:/usr/local/lib/coq/plugins/funind:/usr/local/lib/coq/plugins/rtauto:/usr/local/lib/coq/plugins/micromega:/usr/local/lib/coq/plugins/fourier:/usr/local/lib/coq/plugins/omega:/usr/local/lib/coq/plugins/btauto:/usr/local/lib/coq/plugins/syntax:/usr/local/lib/coq/plugins/decl_mode:/usr/local/lib/coq/plugins/extraction:/usr/local/lib/coq/plugins/cc:/usr/local/lib/coq/plugins/ssrmatching:/usr/local/lib/coq/plugins/nsatz:/usr/local/lib/coq/plugins/quote:/usr/local/lib/coq/plugins/romega:/usr/local/lib/coq/toploop
Makefile:422: recipe for target 'monoid.vo' failed
make: *** [monoid.vo] Error 1

Seems it is complaining about missing the ra_common.cmxs file. Any idea why/how to solve this problem?

Thanks in advance!

Unable to compile with coq 8.12.0 and 8.13.0

Hi! I'm trying to get up and running with this library. I installed it following the README and opam shows coq as version 8.12.0 and coq-relation-algebra as 1.7.4. I have also tried versions 8.13.0 and 1.7.5. I tried running imp.v but it fails at the require import line with:

Unable to locate library kat. (While searching for a .vos file.)

Running make produces the following error:

File "ra_common.ml", line 92, characters 51-107:
Error: This expression has type
         < constant : 'a; dterm : 'b; level : 'c; name : 'd; pattern : 'e;
           reference : 'f; tacexpr : 'g; term : 'h >
         Ltac_plugin.Tacexpr.gen_tactic_arg
       but an expression was expected of type
         < constant : 'i; dterm : 'j; level : 'k; name : 'l; pattern : 'm;
           reference : 'n; tacexpr : 'o; term : 'p >
         Ltac_plugin.Tacexpr.gen_tactic_arg CAst.t
make[1]: *** [Makefile.coq:668: ra_common.cmx] Error 2
make: *** [Makefile.coq:343: all] Error 2

Any ideas on how to go about fixing this? Thanks!

relation algebra segfaults (fails to compile) on latest MacOS (Sonoma > 14.3.X)

There is a strange effect with latest MacOS (14.3.X and 14.4.X): coqc segfaults when compiling theories/normalisation.v. It could also be caused by a change in XCode (still checking). It might well be that this is only reproducible with release binaries. This has been reproduced by several people.

In case you don't have a Mac at this OS version, we can do a remote session and look into this together.

A few notes:

it is not a stack overflow, but an access to an invalid pointer
good instructions for creating a core dump on MacOS can be found here . applying the codesign command on the opam provided coqc did work for me.
a core dump can be inspected on MacOS with lldb -c coredump
this currently kills the MacOS CI for Coq Platform

The codeline which crashes is the fold_expr l in

relation-algebra/theories/normalisation.v

Line 86 in dbb5713

fold_expr l. rewrite <- IHx1 by solve_lower'. lattice.

The resulting stack trace is:

* thread #1, stop reason = ESR_EC_DABORT_EL0 (fault address: 0xfffffffffffffffd)
  * frame #0: 0x0000000102ef6a24 coqc`camlTyping__execute_2270 + 1052
    frame #1: 0x00000001033772bc coqc`camlCArray__fold_left_map_1815 + 276
    frame #2: 0x0000000102ef7080 coqc`camlTyping__execute_2270 + 2680
    frame #3: 0x00000001033772bc coqc`camlCArray__fold_left_map_1815 + 276
    frame #4: 0x0000000102ef7080 coqc`camlTyping__execute_2270 + 2680
    frame #5: 0x0000000102b28cd8 coqc`camlTactics__anon_fn$5btactics$2eml$3a344$2c35$2d$2d489$5d_63511 + 48
    frame #6: 0x0000000102c8f27c coqc`camlRefine__f_666 + 20
    frame #7: 0x0000000102c8f080 coqc`camlRefine__anon_fn$5brefine$2eml$3a109$2c28$2d$2d149$5d_7897 + 24
    frame #8: 0x0000000102c8f00c coqc`camlRefine__anon_fn$5brefine$2eml$3a108$2c27$2d$2d189$5d_7961 + 52
    frame #9: 0x0000000102c8dd60 coqc`camlRefine__anon_fn$5blogic_monad$2eml$3a193$2c15$2d$2d96$5d_54217 + 56
    frame #10: 0x000000010301de38 coqc`camlLogic_monad__anon_fn$5blogic_monad$2eml$3a261$2c15$2d$2d254$5d_1045 + 104
    frame #11: 0x000000010301de38 coqc`camlLogic_monad__anon_fn$5blogic_monad$2eml$3a261$2c15$2d$2d254$5d_1045 + 104
    frame #12: 0x000000010301b6e4 coqc`camlLogic_monad__anon_fn$5blogic_monad$2eml$3a67$2c24$2d$2d45$5d_22570 + 60
    frame #13: 0x000000010301ba18 coqc`camlLogic_monad__anon_fn$5blogic_monad$2eml$3a67$2c24$2d$2d45$5d_108 + 40
    frame #14: 0x000000010301caf8 coqc`camlLogic_monad__run_498 + 40
    frame #15: 0x0000000102c96220 coqc`camlProof__run_tactic_1412 + 248
    frame #16: 0x0000000102c988fc coqc`camlProof__solve_2404 + 1516
    frame #17: 0x0000000102abd9c8 coqc`camlComTactic__anon_fn$5bcomTactic$2eml$3a46$2c57$2d$2d435$5d_1056 + 112
    frame #18: 0x0000000102abd678 coqc`camlComTactic__solve_core_98 + 288
    frame #19: 0x00000001029dd5c8 coqc`camlVernacextend__anon_fn$5bvernacextend$2eml$3a151$2c22$2d$2d125$5d_324 + 24
    frame #20: 0x0000000102aa3cdc coqc`camlVernacinterp__interp_expr_400 + 1300
    frame #21: 0x0000000102aa4654 coqc`camlVernacinterp__anon_fn$5bvernacinterp$2eml$3a158$2c4$2d$2d444$5d_832 + 620
    frame #22: 0x00000001032f3b1c coqc`camlFlags__silently_349 + 92
    frame #23: 0x0000000102aa4cf4 coqc`camlVernacinterp__interp_inner_1098 + 268
    frame #24: 0x00000001026c3e3c coqc`camlStm__step_103662 + 980
    frame #25: 0x00000001026b87a8 coqc`camlStm__define_inner_4277 + 1432
    frame #26: 0x00000001026c36f0 coqc`camlStm__reach_inner_54728 + 4264
    frame #27: 0x00000001026c7a28 coqc`camlStm__observe_11877 + 152
    frame #28: 0x000000010268152c coqc`camlVernac__interp_vernac_145 + 268
    frame #29: 0x0000000102681a5c coqc`camlVernac__loop_1785 + 964
    frame #30: 0x0000000102682410 coqc`camlVernac__load_vernac_520 + 384
    frame #31: 0x000000010268e150 coqc`camlCcompile__compile_37 + 1384
    frame #32: 0x000000010268ea90 coqc`camlCoqc__coqc_run_68 + 304
    frame #33: 0x000000010267d348 coqc`camlDune__exe__Coqc_bin__code_begin + 688
    frame #34: 0x0000000102637294 coqc`caml_program + 11532
    frame #35: 0x000000010343abf4 coqc`caml_start_program + 104
    frame #36: 0x0000000103415de8 coqc`caml_startup_common(argv=0x0000000000000003, pooling=<unavailable>) at startup_nat.c:160:9 [opt]
    frame #37: 0x0000000103415e5c coqc`caml_main [inlined] caml_startup_exn(argv=<unavailable>) at startup_nat.c:167:10 [opt]
    frame #38: 0x0000000103415e54 coqc`caml_main [inlined] caml_startup(argv=<unavailable>) at startup_nat.c:172:15 [opt]
    frame #39: 0x0000000103415e54 coqc`caml_main(argv=<unavailable>) at startup_nat.c:179:3 [opt]
    frame #40: 0x0000000103415ebc coqc`main(argc=<unavailable>, argv=<unavailable>) at main.c:37:3 [opt]
    frame #41: 0x0000000198fba0e0 dyld`start + 2360

@damien-pous (just in case you don't receive notifications for your projects - which happens)

status of example files in the library

@damien-pous : a note on our "smoke test kit" (a quick check Coq Platform does to check if all packages are installed properly): I selected the files compiler_opts.v and imp.v for smoke testing which appear to be examples and coqc reasonably fast. I would appreciate if in a future release you could change these files such that they use From RelationAlgebra Require ... to require modules from you package (you can link this to . in your _CoqProject file). As is I need to patch the files for smoke testing. This would be also useful for users trying your examples, because as is they won't run with an opam installed coq-relation-algebra.

Originally posted by @MSoegtropIMC in coq/platform#167 (comment)

Compilation error with Coq 8.5.0

Today the OPAM bench made the following installation error with Coq 8.5.0 and Relation Algebra 1.4:

# Installed packages for system:
base-bigarray   base  Bigarray library distributed with the OCaml compiler
base-threads    base  Threads library distributed with the OCaml compiler
base-unix       base  Unix library distributed with the OCaml compiler
camlp5          6.14  Preprocessor-pretty-printer of OCaml
coq            8.5.0  Formal proof management system.
The following actions will be performed:
  - install coq-relation-algebra 1.4
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-relation-algebra: http] Command started
[coq-relation-algebra: http] Command started
[coq-relation-algebra.1.4] https://github.com/damien-pous/relation-algebra/archive/v1.4.tar.gz downloaded
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-relation-algebra: coq_makefile Make] Command started
[coq-relation-algebra: make] Command started
[ERROR] The compilation of coq-relation-algebra failed at "make -j6".
[coq-relation-algebra: rm] Command started
#=== ERROR while installing coq-relation-algebra.1.4 ==========================#
# opam-version         1.2.2
# os                   linux
# command              make -j6
# path                 /home/bench/.opam/system/build/coq-relation-algebra.1.4
# compiler             system (4.02.3)
# exit-code            2
# env-file             /home/bench/.opam/system/build/coq-relation-algebra.1.4/coq-relation-algebra-22027-c61e7b.env
# stdout-file          /home/bench/.opam/system/build/coq-relation-algebra.1.4/coq-relation-algebra-22027-c61e7b.out
# stderr-file          /home/bench/.opam/system/build/coq-relation-algebra.1.4/coq-relation-algebra-22027-c61e7b.err
### stdout ###
# [...]
# "coqc"  -q  -R "." RelationAlgebra -I "."   ordinal
# "coqc"  -q  -R "." RelationAlgebra -I "."   lattice
# "coqc"  -q  -R "." RelationAlgebra -I "."   denum
# "coqc"  -q  -R "." RelationAlgebra -I "."   pair
# "coqc"  -q  -R "." RelationAlgebra -I "."   monoid
# "coqc"  -q  -R "." RelationAlgebra -I "."   prop
# "coqc"  -q  -R "." RelationAlgebra -I "."   lset
# "coqc"  -q  -R "." RelationAlgebra -I "."   sups
# "coqc"  -q  -R "." RelationAlgebra -I "."   lsyntax
# Makefile:456: recipe for target 'monoid.vo' failed
### stderr ###
# *** Warning: kat_reification.mllib already found in . (discarding ./kat_reification.mllib)
# File "./monoid.v", line 515, characters 0-28:
# Error: while loading ./ra_fold.cmxs: interface mismatch on Ra_common
# make: *** [monoid.vo] Error 1
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install coq-relation-algebra 1.4
No changes have been performed

I do not know if this bug is reproducible or related to the parallel make -j6.

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.