rocq-elpi 3.3.1

[BrewTestBot]

Created by brew bump

---

Created with brew bump-formula-pr.

• resource blocks have been checked for updates.

---

[chenrui333]

  302 |           try Elpi.API.BuiltIn.of_file id
                      ^^^^^^^^^^^^^^^^^^^^^^^^
  Error: Unbound value Elpi.API.BuiltIn.of_file
  (cd _build/default && /home/linuxbrew/.linuxbrew/opt/ocaml/bin/ocamlc.opt -w -40 -w -27 -g -bin-annot -bin-annot-occurrences -I src/.elpi_plugin.objs/byte -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/compiler -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/lexer_config -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/parser -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/runtime -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/trace/runtime -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/util -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/menhirLib -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/ppx_deriving/runtime -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/re -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/re/str -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/stdlib-shims -I /home/linuxbrew/.linuxbrew/lib/ocaml/dynlink -I /home/linuxbrew/.linuxbrew/lib/ocaml/findlib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/boot -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/clib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/config -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/engine -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/gramlib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/interp -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/kernel -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/lib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/library -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/parsing -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/perf -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/plugins/ltac -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/pretyping -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/printing -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/proofs -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/tactics -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/vernac -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/vm -I /home/linuxbrew/.linuxbrew/lib/ocaml/str -I /home/linuxbrew/.linuxbrew/lib/ocaml/threads -I /home/linuxbrew/.linuxbrew/lib/ocaml/unix -I /home/linuxbrew/.linuxbrew/lib/ocaml/zarith -cmi-file src/.elpi_plugin.objs/byte/elpi_plugin__Rocq_elpi_builtins.cmi -no-alias-deps -open Elpi_plugin -o src/.elpi_plugin.objs/byte/elpi_plugin__Rocq_elpi_builtins.cmo -c -impl src/rocq_elpi_builtins.pp.ml)
  File "src/rocq_elpi_builtins.ml", line 1738, characters 4-34:
  1738 |     coq_print pp Feedback.msg_info
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Error: This expression has type
           Elpi.API.Data.term list ->
           depth:int ->
           unit ->
           unit -> Elpi.API.Data.state -> Elpi.API.Data.state * unit * 'a list
         but an expression was expected of type
           Elpi.API.Data.term list ->
           depth:int ->
           unit -> unit -> Elpi.API.Data.state -> Elpi.API.Data.state * unit
         Type Elpi.API.Data.state * unit * 'a list is not compatible with type
           Elpi.API.Data.state * unit
  (cd _build/default && /home/linuxbrew/.linuxbrew/opt/ocaml/bin/ocamlopt.opt -w -40 -w -27 -g -I src/.elpi_plugin.objs/byte -I src/.elpi_plugin.objs/native -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/compiler -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/lexer_config -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/parser -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/runtime -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/trace/runtime -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/elpi/util -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/menhirLib -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/ppx_deriving/runtime -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/re -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/re/str -I /home/linuxbrew/.linuxbrew/Cellar/rocq-elpi/3.3.1/libexec/ocaml-system/lib/stdlib-shims -I /home/linuxbrew/.linuxbrew/lib/ocaml/dynlink -I /home/linuxbrew/.linuxbrew/lib/ocaml/findlib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/boot -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/clib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/config -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/engine -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/gramlib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/interp -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/kernel -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/lib -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/library -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/parsing -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/perf -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/plugins/ltac -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/pretyping -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/printing -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/proofs -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/tactics -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/vernac -I /home/linuxbrew/.linuxbrew/lib/ocaml/rocq-runtime/vm -I /home/linuxbrew/.linuxbrew/lib/ocaml/str -I /home/linuxbrew/.linuxbrew/lib/ocaml/threads -I /home/linuxbrew/.linuxbrew/lib/ocaml/unix -I /home/linuxbrew/.linuxbrew/lib/ocaml/zarith -cmi-file src/.elpi_plugin.objs/byte/elpi_plugin__Rocq_elpi_builtins.cmi -no-alias-deps -open Elpi_plugin -o src/.elpi_plugin.objs/native/elpi_plugin__Rocq_elpi_builtins.cmx -c -impl src/rocq_elpi_builtins.pp.ml)
  File "src/rocq_elpi_builtins.ml", line 1738, characters 4-34:
  1738 |     coq_print pp Feedback.msg_info
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Error: This expression has type
           Elpi.API.Data.term list ->
           depth:int ->
           unit ->
           unit -> Elpi.API.Data.state -> Elpi.API.Data.state * unit * 'a list
         but an expression was expected of type
           Elpi.API.Data.term list ->
           depth:int ->
           unit -> unit -> Elpi.API.Data.state -> Elpi.API.Data.state * unit
         Type Elpi.API.Data.state * unit * 'a list is not compatible with type
           Elpi.API.Data.state * unit

[cho-m]

Likely need to update resources. May check if there is a better way to handle. Though I think there are still limitations here as the dependency is expressed via a opam-style conditional so not that straightforward to autodetect versioning.

[github-actions]

This pull request has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. To keep this pull request open, add a help wanted or in progress label.

[github-actions]

🤖 An automated task has requested bottles to be published to this PR.

Caution

Please do not push to this PR branch before the bottle commits have been pushed, as this results in a state that is difficult to recover from. If you need to resolve a merge conflict, please use a merge commit. Do not force-push to this PR branch.