[new release] orthologic-coq (0.9)

[SimonGuilloud]

A plugin to add orthologic-based tactics to Coq

• Project page: https://github.com/SimonGuilloud/orthologic-coq

CHANGES:

Initial Release.

[mseri]

The build currently fails with

# (cd _build/default && /home/opam/.opam/5.3/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /home/opam/.opam/5.3/lib/findlib -I /home/opam/.opam/5.3/lib/ocaml/dynlink -I /home/opam/.opam/5.3/lib/ocaml/str -I /home/opam/.opam/5.3/lib/ocaml/threads -I /home/opam/.opam/5.3/lib/ocaml/unix -I /home/opam/.opam/5.3/lib/rocq-runtime/boot -I /home/opam/.opam/5.3/lib/rocq-runtime/clib -I /home/opam/.opam/5.3/lib/rocq-runtime/config -I /home/opam/.opam/5.3/lib/rocq-runtime/engine -I /home/opam/.opam/5.3/lib/rocq-runtime/gramlib -I /home/opam/.opam/5.3/lib/rocq-runtime/interp -I /home/opam/.opam/5.3/lib/rocq-runtime/kernel -I /home/opam/.opam/5.3/lib/rocq-runtime/lib -I /home/opam/.opam/5.3/lib/rocq-runtime/library -I /home/opam/.opam/5.3/lib/rocq-runtime/parsing -I /home/opam/.opam/5.3/lib/rocq-runtime/perf -I /home/opam/.opam/5.3/lib/rocq-runtime/plugins/ltac -I /home/opam/.opam/5.3/lib/rocq-runtime/pretyping -I /home/opam/.opam/5.3/lib/rocq-runtime/printing -I /home/opam/.opam/5.3/lib/rocq-runtime/proofs -I /home/opam/.opam/5.3/lib/rocq-runtime/tactics -I /home/opam/.opam/5.3/lib/rocq-runtime/vernac -I /home/opam/.opam/5.3/lib/rocq-runtime/vm -I /home/opam/.opam/5.3/lib/zarith -I src -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/btauto -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/cc -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/cc_core -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/derive -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/extraction -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/firstorder -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/firstorder_core -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/funind -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/ltac -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/ltac2 -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/ltac2_ltac1 -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/micromega -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/micromega_core -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/nsatz -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/nsatz_core -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/number_string_notation -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/ring -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/rtauto -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/ssreflect -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/ssrmatching -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/tauto -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/tutorial/p0 -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/tutorial/p1 -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/tutorial/p2 -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/tutorial/p3 -I /home/opam/.opam/5.3/lib/coq/../rocq-runtime/plugins/zify -R /home/opam/.opam/5.3/lib/coq/theories Coq -R theories OLCoq theories/OL_Theory.v)
# File "./theories/OL_Theory.v", line 2, characters 15-18:
# Error: Cannot find a physical path bound to logical path Lia.
# 
# (cd _build/default && /home/opam/.opam/5.3/bin/ocamlc.opt -w -40 -w -27 -g -bin-annot -bin-annot-occurrences -I src/.OLCoq.objs/byte -I /home/opam/.opam/5.3/lib/findlib -I /home/opam/.opam/5.3/lib/ocaml/dynlink -I /home/opam/.opam/5.3/lib/ocaml/str -I /home/opam/.opam/5.3/lib/ocaml/threads -I /home/opam/.opam/5.3/lib/ocaml/unix -I /home/opam/.opam/5.3/lib/rocq-runtime/boot -I /home/opam/.opam/5.3/lib/rocq-runtime/clib -I /home/opam/.opam/5.3/lib/rocq-runtime/config -I /home/opam/.opam/5.3/lib/rocq-runtime/engine -I /home/opam/.opam/5.3/lib/rocq-runtime/gramlib -I /home/opam/.opam/5.3/lib/rocq-runtime/interp -I /home/opam/.opam/5.3/lib/rocq-runtime/kernel -I /home/opam/.opam/5.3/lib/rocq-runtime/lib -I /home/opam/.opam/5.3/lib/rocq-runtime/library -I /home/opam/.opam/5.3/lib/rocq-runtime/parsing -I /home/opam/.opam/5.3/lib/rocq-runtime/perf -I /home/opam/.opam/5.3/lib/rocq-runtime/plugins/ltac -I /home/opam/.opam/5.3/lib/rocq-runtime/pretyping -I /home/opam/.opam/5.3/lib/rocq-runtime/printing -I /home/opam/.opam/5.3/lib/rocq-runtime/proofs -I /home/opam/.opam/5.3/lib/rocq-runtime/tactics -I /home/opam/.opam/5.3/lib/rocq-runtime/vernac -I /home/opam/.opam/5.3/lib/rocq-runtime/vm -I /home/opam/.opam/5.3/lib/zarith -no-alias-deps -open OLCoq -o src/.OLCoq.objs/byte/oLCoq__Ce_api.cmo -c -impl src/ce_api.ml)
# File "src/ce_api.ml", line 22, characters 81-95:
# 22 | let lib_constr n = lazy (UnivGen.constr_of_monomorphic_global (Global.env ()) @@ Coqlib.lib_ref n)
#                                                                                       ^^^^^^^^^^^^^^
# Alert deprecated: module Coqlib
# (9.0) Use Rocqlib
# 
# File "src/ce_api.ml", line 24, characters 21-42:
# 24 | let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
#                           ^^^^^^^^^^^^^^^^^^^^^
# Error: Unbound value "Coqlib.find_reference"

[SimonGuilloud]

Sorry I'm not sure what is the issue, if there is one. I have simply followed https://github.com/tarides/dune-release. dune build succeeds (including in a fresh docker image) and so does dune-release check.

[SimonGuilloud]

Thanks !