2020-07-12 23:25:37 (GMT)
should we prepare a merge onto master from a stable-ish branch (combinators?) and tag it 2.0? :)
Full boolean support can be in 2.1, I think the success at CASC warrants a stable release that people can use and benchmark against.
2020-07-13 9:28:0 (GMT)
I agree.
Also, I need to sift through the configurations, find ones that perform well in general and have a small manual on how to use
Zip with this parameters.
2020-07-14 12:44:23 (GMT)
BTW there's already something that calls itself "Zipperpin 2.0" on System on TPTP. In the interest of promoting sanity, I would propose that you call your release 2.0.1 or 2.1 or whatever but not 2.0 unless it corresponds exactly with that.
2020-07-14 12:44:43 (GMT)
Or even 2.0.0. ;)
2020-07-14 13:28:56 (GMT)
Yes indeed. I think the CASC version could have been 2.0-casc-2020 or something like that, but it's ok, we can just release 2.1 or 2.0.1 :slight_smile:
2020-10-13 14:5:6 (GMT)
So, it would be nice to do 2.1 some time? There's still no official downloadable 2.0 anywhere, even on github, where 1.6 is the latest. That's not a very good look imho…
2020-10-14 16:19:17 (GMT)
Simon Cruanes said:
So, it would be nice to do 2.1 some time? There's still no official downloadable 2.0 anywhere, even on github, where 1.6 is the latest. That's not a very good look imho…
Definitely, but I am personally extremely busy with several papers in my pipeline. I will get back to you when I am more ready to release
2020-10-14 16:20:15 (GMT)
What about OPAM? Will you update the package? Makarius (the Isabelle release manager) wants to include Zipperposition in the next Isabelle -- it would be convenient to do it over OPAM and not directly from the source.
2020-10-14 16:20:39 (GMT)
We need the version where Petar adapted the proof output to THF.
2020-10-14 16:46:0 (GMT)
When was that? And what branch? A merge into master should not be that hard, or we did something wrong somewhere. The release itself I can do, I think.
2020-10-14 17:1:56 (GMT)
OK. The branch ho-techniques-paper is the latest stable branch
2020-10-14 17:2:0 (GMT)
you can release using this branch
2020-10-14 17:2:18 (GMT)
( I think, let me double check this )
2020-10-17 15:56:2 (GMT)
Ok, tell me what you think, and I'll merge and release soon after.
2020-12-10 20:2:31 (GMT)
Release is ongoing on https://github.com/ocaml/opam-repository/pull/17807 . Please try and build it, y'all!
2020-12-11 13:3:41 (GMT)
Ohoh:
$ opam install zipperposition.2.0
The following actions will be performed:
∗ install logtk 2.0 [required by zipperposition]
∗ install libzipperposition 2.0 [required by zipperposition]
∗ install zipperposition 2.0
===== ∗ 3 =====
Do you want to continue? [Y/n] y
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[libzipperposition.2.0] downloaded from cache at https://opam.ocaml.org/cache
[logtk.2.0] downloaded from cache at https://opam.ocaml.org/cache
[zipperposition.2.0] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[ERROR] The compilation of logtk failed at "/Users/alex/.opam/opam-init/hooks/sandbox.sh build dune build -p logtk -j 4".
#=== ERROR while compiling logtk.2.0 ==========================================#
# context 2.0.0 | macos/x86_64 | ocaml-variants.4.10.0+flambda | https://opam.ocaml.org/#08e27c9d
# path ~/.opam/4.10.0+flambda/.opam-switch/build/logtk.2.0
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p logtk -j 4
# exit-code 65
# env-file ~/.opam/log/logtk-9941-8c0dd3.env
# output-file ~/.opam/log/logtk-9941-8c0dd3.out
### output ###
# /Users/alex/.opam/opam-init/hooks/sandbox.sh: line 8: cd: /Users/alex/.ccache: No such file or directory
# sandbox-exec: empty subpath pattern
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
┌─ The following actions failed
│ λ build logtk 2.0
└─
╶─ No changes have been performed
2020-12-11 16:7:20 (GMT)
I'll wait until I know this has been solved to test on the Mac I guess.
2020-12-11 16:8:28 (GMT)
You can try. Maybe something is wrong with my setup, e.g. the ocaml version I am using?
2020-12-11 16:9:22 (GMT)
Well I'm busy reading a thesis intro.
2020-12-11 16:9:58 (GMT)
Oh, that should definitely have priority :grinning:
2020-12-11 16:18:7 (GMT)
Done.
2020-12-11 17:1:22 (GMT)
Alexander Bentkamp said:
You can try. Maybe something is wrong with my setup, e.g. the ocaml version I am using?
The version seems fine, seems more like a opam sandboxing issue. Maybe open a ticket on opam? :/
2020-12-11 17:32:4 (GMT)
Did I miss some instructions? I'm ready to test on the Mac but opam install zipperposition.2.0 says there's no such version.
2020-12-11 17:32:20 (GMT)
opam update first
2020-12-11 17:33:47 (GMT)
I got a new error now:
$ opam install zipperposition.2.0
The following actions will be performed:
∗ install logtk 2.0 [required by zipperposition]
∗ install libzipperposition 2.0 [required by zipperposition]
∗ install zipperposition 2.0
===== ∗ 3 =====
Do you want to continue? [Y/n] y
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[libzipperposition.2.0] found in cache
[logtk.2.0] found in cache
[zipperposition.2.0] found in cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
∗ installed logtk.2.0
[ERROR] The compilation of libzipperposition failed at "/Users/alex/.opam/opam-init/hooks/sandbox.sh build dune build -p libzipperposition -j 4".
#=== ERROR while compiling libzipperposition.2.0 ==============================#
# context 2.0.0 | macos/x86_64 | ocaml-variants.4.10.0+flambda | https://opam.ocaml.org/#08e27c9d
# path ~/.opam/4.10.0+flambda/.opam-switch/build/libzipperposition.2.0
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p libzipperposition -j 4
# exit-code 1
# env-file ~/.opam/log/libzipperposition-29725-1c6298.env
# output-file ~/.opam/log/libzipperposition-29725-1c6298.out
### output ###
# [...]
# ocamlc src/prover_calculi/.libzipperposition_calculi.objs/byte/libzipperposition_calculi__Bce.{cmo,cmt} (exit 2)
# (cd _build/default && /Users/alex/.opam/4.10.0+flambda/bin/ocamlc.opt -w -40 -warn-error -3+8 -w -3 -color always -safe-string -w -32 -g -bin-annot -I src/prover_calculi/.libzipperposition_calculi.objs/byte -I /Users/alex/.opam/4.10.0+flambda/lib/bytes -I /Users/alex/.opam/4.10.0+flambda/lib/containers -I /Users/alex/.opam/4.10.0+flambda/lib/containers-data -I /Users/alex/.opam/4.10.0+flambda[...]
# File "src/prover_calculi/bce.ml", line 89, characters 29-43:
# 89 | module TaskPriorityQueue = CCMutHeap.Make(TaskWrapper)
# ^^^^^^^^^^^^^^
# Error: Unbound module CCMutHeap
# ocamlopt src/prover_calculi/.libzipperposition_calculi.objs/native/libzipperposition_calculi__Bce.{cmx,o} (exit 2)
# (cd _build/default && /Users/alex/.opam/4.10.0+flambda/bin/ocamlopt.opt -w -40 -warn-error -3+8 -w -3 -color always -safe-string -w -32 -g -O3 -unbox-closures -unbox-closures-factor 20 -I src/prover_calculi/.libzipperposition_calculi.objs/byte -I src/prover_calculi/.libzipperposition_calculi.objs/native -I /Users/alex/.opam/4.10.0+flambda/lib/bytes -I /Users/alex/.opam/4.10.0+flambda/lib/cont[...]
# File "src/prover_calculi/bce.ml", line 89, characters 29-43:
# 89 | module TaskPriorityQueue = CCMutHeap.Make(TaskWrapper)
# ^^^^^^^^^^^^^^
# Error: Unbound module CCMutHeap
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
┌─ The following actions failed
│ λ build libzipperposition 2.0
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install logtk 2.0
└─
The former state can be restored with:
opam switch import "/Users/alex/.opam/4.10.0+flambda/.opam-switch/backup/state-20201211172859.export"
2020-12-11 17:37:18 (GMT)
Ah @Petar Vukmirovic did use the mutable heap in this branch? damn.
Try opam pin containers 3.1
2020-12-11 17:42:6 (GMT)
ok, I did opam upgrade instead, but it works now! :tada:
2020-12-14 13:36:43 (GMT)
On the Mac, problems with containers:
#=== ERROR while compiling containers.3.1 =====================================#
# context 2.0.5 | macos/x86_64 | ocaml-base-compiler.4.10.0 | https://opam.ocaml.org#98d4cda0
# path ~/.opam/4.10.0/.opam-switch/build/containers.3.1
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p containers -j 4
# exit-code 1
# env-file ~/.opam/log/containers-24576-9e78df.env
# output-file ~/.opam/log/containers-24576-9e78df.out
### output ###
# [...]
# File "caml_startup", line 1:
# Error: Error during linking
# ocamlopt src/mkflags.exe (exit 2)
# (cd _build/default && /Users/blanchette/.opam/4.10.0/bin/ocamlopt.opt -w -40 -warn-error -3 -g -o src/mkflags.exe /Users/blanchette/.opam/4.10.0/lib/ocaml/unix.cmxa -I /Users/blanchette/.opam/4.10.0/lib/ocaml /Users/blanchette/.opam/4.10.0/lib/dune-private-libs/dune_csexp/dune_csexp.cmxa /Users/blanchette/.opam/4.10.0/lib/dune-configurator/configurator.cmxa src/.mkflags.eobjs/native/mkflags.cmx)
# Undefined symbols for architecture x86_64:
# "___darwin_check_fd_set_overflow", referenced from:
# _unix_select in libunix.a(select.o)
# _fdset_to_fdlist in libunix.a(select.o)
# ld: symbol(s) not found for architecture x86_64
# clang: error: linker command failed with exit code 1 (use -v to see invocation)
# File "caml_startup", line 1:
# Error: Error during linking
2020-12-14 16:11:57 (GMT)
is this on a fresh switch? never seen that before… can you compile any OCaml program?
say:
let () = print_endline "hello"
in foo.ml, then ocamlopt foo.ml -o foo and try to run foo?
2020-12-14 16:29:52 (GMT)
That works. I get "foo".
2020-12-14 16:37:37 (GMT)
If it helps, I could have a live debugging session with you. But that would be in a few hours from now, or tomorrow.
2020-12-14 16:37:46 (GMT)
Have a PhD thesis to read by 10:00 tomorrow morning.
2020-12-14 16:52:2 (GMT)
I can't promise full interactivity but sure, let's do it!
2020-12-14 16:55:53 (GMT)
I can't tell you exactly when I can, but I'll just write here and see when you pop up.
2020-12-14 16:56:0 (GMT)
Right now I need to make a bit more progress in the thesis.
2020-12-14 17:31:0 (GMT)
Let me know when you have a sec. ;)
2020-12-14 17:31:6 (GMT)
I could do with a break. ;)
2020-12-14 18:3:3 (GMT)
Maybe in a few hours? :s
2020-12-14 18:6:45 (GMT)
Sure.
2020-12-14 18:16:1 (GMT)
Shall we say 3PM / 9PM?
2020-12-14 18:16:9 (GMT)
Makes planning easier. ;)
2020-12-14 18:16:55 (GMT)
sounds good.