search

coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
188 stars 49 forks source link

Add CoqHammer (and ATPs) to the Coq Platform #10

Closed palmskog closed 2 years ago

palmskog commented 4 years ago

CoqHammer nowadays consists of two components, where the first can be used independently of the second:

  1. a general proof search procedure for CIC, sauto (package coq-hammer-tactics), and
  2. an automated reasoning system which calls ATPs with selected premises and tries to reconstruct ATP proofs (package coq-hammer).

The latest version of these components and packages, 1.3, are available for Coq 8.10, 8.11, and 8.12.

CoqHammer provides much-needed high-level proof automation for Coq users. It is part of Coq's CI and has had consistent releases matching Coq's major versions since Coq 8.8, all of which are packaged on the Coq opam archive. I propose that CoqHammer should be included in the Coq platform, along with at least two ATPs, e.g., Z3 and Eprover.

The maintainer of CoqHammer is @lukaszcz.

spitters commented 3 years ago

Discussion here suggests that it may be possible to add vampire too. https://coq.discourse.group/t/what-does-it-mean-that-isabelle-has-better-automation-than-coq/957/14

MSoegtropIMC commented 3 years ago

I am currently looking into this package (late enough ...).

One question: there is an opam z3 package, which looks reasonably well maintained. The only rather odd thing about it is that it requires Python 2.7. Is it really so that z3 requires python 2.7 or is this a wrong dependency in the opam file (say it could live with a 3.x python instead as well).

I ask because these days it can be messy to require python2. Usually just "python" is now python3 on many systems, but many packages requiring python2 require that "python" is python2.

Any another question: shoudl Coq Platform just add z3 and leave it to the user to add additional provers as needed or do you have other preferences?

MSoegtropIMC commented 3 years ago

@lukaszcz, @palmskog : I just created an Opam package for E (there already is one for z3). I wonder how I can test if coq-hammer detects the various backend provers. Should I disable one or the other and try if the examples of coq-hammer still work?

lukaszcz commented 3 years ago

First, the z3 package might be useless for our purposes, because CoqHammer requires a custom TPTP backend which is not distributed by default (see https://coqhammer.github.io/#installation-of-first-order-provers).

The latest versions of CoqHammer (since 1.3.1) when the "hammer" tactic is first called try to detect the provers and print out if that was successful or not for each prover.

On Fri, 24 Sept 2021 at 18:22, MSoegtropIMC @.***> wrote:

@lukaszcz https://github.com/lukaszcz, @palmskog https://github.com/palmskog : I just created an Opam package for E (there already is one for z3). I wonder how I can test if coq-hammer detects the various backend provers. Should I disable one or the other and try if the examples of coq-hammer still work?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/10#issuecomment-926760501, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKHZEKDNN2AOLDJYRF5TUDSQUJANCNFSM4PVG6NHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

MSoegtropIMC commented 3 years ago

@lukaszcz : thanks for the pointers! I guess it shouldn't be hard to change the z3 opam package such that it also compiles the tptp frontend.

Two more questions:

1.) @palmskog recommended above to install at least z3 and eprover, in the link you shared you recommend to install at least vampire and CVC4 - which leaves me in confusion ...

2.) The Windows installer (in the future also Mac) derives the dependencies between choosable packages from opam. The installer automatically selects and deselects packages accordingly and notifies the user about the dependencies. coq-hammer currently has no opam level dependencies to ATPs - likely because there are no usable opam packages. Assuming I manage to create usable opam packages (the eprover package looks fine and I had the impression that the z3 package did work as it is - at least the coq-hammer tutorial did work with just opam z3 installed) should the coq-hammer opam package depend on these? If not, how shall this be handled in the Windows installer? Should the ATP packages be independently selectable by the user relying on that the user knows what (s)he is doing?

palmskog commented 3 years ago

@MSoegtropIMC my old recommendation was for z3 and Eprover mostly because they were open source and together could give good results, and Eprover seemed the easiest to build/install. Now, Vampire has been open sourced, and I think Łukasz has a better view of what one should pick when the playing field is open.

MSoegtropIMC commented 3 years ago

@palmskog : thanks, I try my luck with eprover and z3_tptp then and add vampire later.

But I still don't get it. I am trying the examples in (https://github.com/lukaszcz/coqhammer/tree/coq8.13/examples/tutorial/hammer) and no matter if I have z3_tptp and/or eprover or not in the path, these examples run through fine without errors. Where is an example which actually requires an external ATP?

palmskog commented 3 years ago

@MSoegtropIMC the idea is that the effects of the running the hammer tactic are not generally reproducible, so anyone playing around with that file has to manually uncomment the hammer tactic call. What actually gets run if you don't uncomment hammer are reconstruction tactics that were found before (and are not guaranteed to be recommended again).

palmskog commented 3 years ago

What I think we can (should) do when the ATPs are well packaged is to set up a CI job for CoqHammer with a test that fails or passes when a certain ATP is present. But I believe this was avoided so far since installing the ATPs is tricky to automate, and depending on which ATP versions and combinations you have, the results are nondeterministic.

lukaszcz commented 3 years ago

1.) @palmskog https://github.com/palmskog recommended above to install at least z3 and eprover, in the link you shared you recommend to install at least vampire and CVC4 - which leaves me in confusion ...

My recommendation is based solely on the fact that Vampire and CVC4 seem to be the strongest ATPs for this application.

2.) The Windows installer (in the future also Mac) derives the dependencies between choosable packages from opam. The installer automatically selects and deselects packages accordingly and notifies the user about the dependencies. coq-hammer currently has no opam level dependencies to ATPs - likely because there are no usable opam packages. Assuming I manage to create usable opam packages (the eprover package looks fine and I had the impression that the z3 package did work as it is - at least the coq-hammer tutorial did work with just opam z3 installed) should the coq-hammer opam package depend on these? If not, how shall this be handled in the Windows installer? Should the ATP packages be independently selectable by the user relying on that the user knows what (s)he is doing?

The status of CoqHammer on Windows is unclear. The code uses some Unix-specific things. It has been tested and maintained only for Mac and Linux. I'm a Mac/Linux user and I don't even have (continuous) access to a Windows machine.

MSoegtropIMC commented 3 years ago

anyone playing around with that file has to manually uncomment the hammer tactic call

Ah thanks, I should have read the fine print :-)

The status of CoqHammer on Windows is unclear.

This makes it difficult...impossible to include it in the "full" level of Coq Platform - we should work on this, since I think it is an important project. Let's see what CI says. For moth Unix APIs there are fairly good emulation layers in Windows - just making use of full blown fork semantics as in OCaml backwards step debugging are rather tricky to do in Windows, but I don't see why one would need this on Windows to run an ATP.

MSoegtropIMC commented 3 years ago

To summarize the current state:

MSoegtropIMC commented 3 years ago

P.S.: I plan to include coq-hammer-tactics also in the 8.14 beta release (which is due soon).

MSoegtropIMC commented 3 years ago

Note: the "postponed" label applies to coq-hammer. coq-hammer-tactics is in 2021.09 8.13 and also planned for 2021.09 8.14+beta.

lukaszcz commented 3 years ago

in the 8.13~2021.09 pick I will include coq-hammer-tactics.1.3.1but not coq-hammerbecause we need to work on opam packages for the ATPs and on the Windows support. I am confident that we can solve this for the 8.14 release which is planned for some time in November.

If you can wait a few days, I'll make a 1.3.2 release which will include an important bugfix.

@lukaszcz : after fixing this, can you setup a Windows test in your CI?

Yes, probably I could do that.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

MSoegtropIMC commented 3 years ago

I plan to do the tag on Friday or Monday. What is your timeline?

lukaszcz commented 3 years ago

I think I'll manage tomorrow, or during the weekend at the latest

On Wed, 29 Sep 2021, 18:11 MSoegtropIMC, @.***> wrote:

I plan to do the tag on Friday or Monday. What is your timeline?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/10#issuecomment-930323216, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKH26HN3626BWMHTAKV3UEM3EDANCNFSM4PVG6NHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

MSoegtropIMC commented 3 years ago

Fine, I will wait then. Just to confirm: the bug fix is in coq-hammer-tactics, not in coq-hammer (the latter is not yet in Coq Platform).

lukaszcz commented 3 years ago

Yes, it's about parsing arguments. And it should be fixed because it may cause syntax errors in unrelated lemma statements

On Wed, 29 Sep 2021, 23:05 MSoegtropIMC, @.***> wrote:

Fine, I will wait then. Just to confirm: the bug fix is in coq-hammer-tactics, not in coq-hammer (the latter is not yet in Coq Platform).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/10#issuecomment-930542992, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKH6C5SLAB5VZYS3K6MTUEN5RTANCNFSM4PVG6NHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

lukaszcz commented 3 years ago

I have created the 1.3.2 release.

On Wed, 29 Sept 2021 at 23:56, Łukasz Czajka @.***> wrote:

Yes, it's about parsing arguments. And it should be fixed because it may cause syntax errors in unrelated lemma statements

On Wed, 29 Sep 2021, 23:05 MSoegtropIMC, @.***> wrote:

Fine, I will wait then. Just to confirm: the bug fix is in coq-hammer-tactics, not in coq-hammer (the latter is not yet in Coq Platform).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/10#issuecomment-930542992, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAAPKH6C5SLAB5VZYS3K6MTUEN5RTANCNFSM4PVG6NHQ . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

MSoegtropIMC commented 2 years ago

I now created Opam packages for z3_tptp and eprover. cvc4 is planned for the Coq 8.15 release (March or so). Coq-hammer now works fine with eprover and z3 on Mac and Linux.