Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Package why3find.1.1.0 #27144

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

btjorge
Copy link
Contributor

@btjorge btjorge commented Dec 18, 2024

why3find.1.1.0

A Why3 Package Manager
The why3find utility is designed for managing packages for why3 developpers and associated OCaml extracted code.



🐫 Pull-request generated by opam-publish v2.5.0

@mseri
Copy link
Member

mseri commented Dec 19, 2024

This looks like a rather brittle test:

#=== ERROR while compiling why3find.1.1.0 =====================================#
# context              2.4.0~alpha1~dev | linux/x86_32 | ocaml-base-compiler.4.14.2 | pinned(https://git.frama-c.com/pub/why3find/-/archive/1.1.0/why3find-1.1.0.tar.gz)
# path                 ~/.opam/4.14/.opam-switch/build/why3find.1.1.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p why3find -j 31 --promote-install-files=false @install @runtest
# exit-code            1
# env-file             ~/.opam/log/why3find-7-9d8847.env
# output-file          ~/.opam/log/why3find-7-9d8847.out
### output ###
# File "tests/proof.t/run.t", line 1, characters 0-0:
# /usr/bin/git --no-pager diff --no-index --color=always -u _build/.sandbox/8c4573b5d9374f33c9d7bd49301d587b/default/tests/proof.t/run.t _build/.sandbox/8c4573b5d9374f33c9d7bd49301d587b/default/tests/proof.t/run.t.corrected
# diff --git a/_build/.sandbox/8c4573b5d9374f33c9d7bd49301d587b/default/tests/proof.t/run.t b/_build/.sandbox/8c4573b5d9374f33c9d7bd49301d587b/default/tests/proof.t/run.t.corrected
# index f2b930a..ba66988 100644
# --- a/_build/.sandbox/8c4573b5d9374f33c9d7bd49301d587b/default/tests/proof.t/run.t
# +++ b/_build/.sandbox/8c4573b5d9374f33c9d7bd49301d587b/default/tests/proof.t/run.t.corrected
# @@ -155,7 +155,7 @@
#    <pre class="src">
#      alt-ergo     @2.4.2  n=16  169ms
#      cvc4         @1.8    n=42  550ms
# -    z3           @4.8.6  n=33  570ms
# +    z3           @4.8.6  n=33  569ms
#    </pre>
#    <h1>Proofs</h1>
#    <pre class="src"><span class="keyword">module</span> <a id="S" href="certif.S.html">certif.S</a><span title="Partial proof (6/10 goals)" class="icon warning icofont-error"></span></pre>

I'd suggest to remove the speed from the output if possible in future releases to make it more robust

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants