[new release] lambdapi (2.5.1)

[fblanqui]

Proof assistant for the λΠ-calculus modulo rewriting

• Project page: https://github.com/Deducteam/lambdapi

CHANGES:

Added

• Add export format raw_dk.
• Fix of the color of the text in command line when console.out is used.
• Use black text instead of red when diplaying query answers.
• Allow negative numbers in notation priorities.
• New release 0.2.2 of the VSCode plugin.

[shonfeder]

Hello! Thanks for the update :)

I see a failure on arm32-ocaml-5.2 and x86_32-ocaml-5.2 (other platforms are ok)

[ERROR] The compilation of lambdapi.2.5.1 failed at "dune build -p lambdapi -j 79 @install".

#=== ERROR while compiling lambdapi.2.5.1 =====================================#
# context              2.3.0~alpha~dev | linux/arm32 | ocaml-base-compiler.5.2.0 | pinned(https://github.com/Deducteam/lambdapi/releases/download/2.5.1/lambdapi-2.5.1.tbz)
# path                 ~/.opam/5.2/.opam-switch/build/lambdapi.2.5.1
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p lambdapi -j 79 @install
# exit-code            1
# env-file             ~/.opam/log/lambdapi-7-393e6d.env
# output-file          ~/.opam/log/lambdapi-7-393e6d.out
### output ###
# File "src/cli/dune", line 2, characters 7-15:
# 2 |  (name lambdapi)
#            ^^^^^^^^
# Error: No rule found for src/cli/lambdapi.exe

Looking at the source and other platforms building correctly, I'm not immediately sure why dune would fail to find the src/cli/lambdapi.ml here. 😕

[mseri]

I was looking into it as well, and I don't really know. It fails on bytecode-only targets, but why I can't understand

[fblanqui]

Hi. It seems that some errors are not related to lambdapi:

• https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/5b0603c50b11a425d94487caa242946e2ceef2a8/variant/extras,opam-2.0-ocaml-4.14,lambdapi.2.5.1
  (failed: Sorry, resolution of the request timed out.)
  I launched a rebuild.
• https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/5b0603c50b11a425d94487caa242946e2ceef2a8/variant/extras,opam-2.1-ocaml-4.14,lambdapi.2.5.1
  Idem.
• https://github.com/ocaml/opam-repository/actions/runs/10038619654/job/27740911560?pr=26270#step:12:246
  [ERROR] Failed to get sources of pratter.3.0.0: Curl failed
  What can we do about this one?

And the others?

[mseri]

Only the 32 bit errors are to be understood, the rest is fine.

And I know why it fails! You are building both native and bytecode executable always. But those platforms are bytecode only, so the build fails trying to make a native executable

[mseri]

Suggested change

	available: arch != "ppc64"
	available: arch != "ppc64"
	conflicts: [ "ocaml-option-bytecode-only" ]

are you sure ppc64 is still needed there and it was not also a failure of the same type?

[fblanqui]

Thank you! I don't know. I'm going to update the PR to check this.

[fblanqui]

Hi. Is it ok now or should I make other changes?

[mseri]

Looks good, thanks