2020-07-14 12:47:48 (GMT)
I'm getting credit where no credit is due. Gerwin Klein wrote:
ps: I like the name :-) But your tools have always had cool names, so I shouldn’t be surprised ;-)
I'll have to disappoint him. To be frank, I've never been such a huge fan of the name Zip, but at least it's unique enough (unlike Lean...), and you know where to find it when you scroll the long list of System on TPTP (or, conversely, the THF division at CASC...).
2020-07-14 13:33:14 (GMT)
To be fair, the name was picked in 2012, and I regret a bit that it's not too accurate. As the readme states, there's not that much functional programming going on in there.
2020-07-14 13:34:4 (GMT)
In the tradition of french programs, it should have had an animal name. I propose "naked mole rat 2.0.1" for the release.
2020-07-14 13:35:36 (GMT)
It's probably just my bad pronunciation, but people always hear "superposition" when I say "zipperposition" :D
2020-07-14 13:37:49 (GMT)
You need to twirl your mustache and exaggerate the "zipper" part when you say it.
2020-07-14 15:1:15 (GMT)
That's not corona conform I'm afraid.
2020-07-14 15:2:23 (GMT)
I was sneakily trying to become a Zip developer when I ran into the following build errors. It was working 2 hours ago. Any idea what's going on? Isabelle was blankly refusing to start earlier today. Definitely a bad hair day. :S
Error: /Users/blanchette/.opam/ocaml/lib/containers/cCFormat.cmx
is not a compilation unit description.
2020-07-14 15:3:52 (GMT)
BTW in TSTP proofs, negated_conjectures are not properly connected to their parent conjecture clauses. Petar and I are on it.
2020-07-14 15:4:14 (GMT)
Trying to integrate Zip in Isabelle reveals interesting issues.
2020-07-14 15:11:15 (GMT)
opam reinstall containers ? maybe?
2020-07-14 15:11:28 (GMT)
Jasmin Blanchette said:
Trying to integrate Zip in Isabelle reveals interesting issues.
Ah, making stuff production ready…
2020-07-14 15:17:58 (GMT)
Thanks. Didn't work though. :S
2020-07-14 15:24:58 (GMT)
How old is your opam switch? Might be worth doing opam sw create 4.08.1 or something like that (I assume you have opam 2).
2020-07-14 15:29:10 (GMT)
I had that switch. As I said, it worked. It just suddenly stopped working. Now doing a fresh install of 4.10.0. All with Petar helping.
2020-07-14 15:32:49 (GMT)
4.10 working so far. Just rebuild Zip. The one that now connects neg_conj with conj. ;)
2020-07-14 15:44:54 (GMT)
As for the "sneakily", it's harder to hide when you push commits to github :p