search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 89 forks source link

easycrypt #43

Closed spitters closed 7 years ago

spitters commented 8 years ago

Currently, adding PG support for easycrypt require a little bit of work. See the README. Perhaps, this can be one of the supported proof assistants?

PG files are here

Personally, I currently have some installation issues. Hence and issue and no pull-request.

cpitclaudel commented 8 years ago

Sure, that would be good :) Do you want to prepare a pull request?

spitters commented 8 years ago

Currently, PG + easycrypt does not install for me.

I am following the system wide installation instructions. easycrypt installs from opam, but when I open an .ec file with emacs, it does not start PG. Nor does it M-x proofgeneral find easycrypt.

I'd prefer not to send a pull request until I have something working on my system.

@cpitclaudel How much of the company-coq magic can be ported to easycrypt? It looks very nice.

cpitclaudel commented 8 years ago

@spitters Can you clarify how you installed PG? Does that procedure work with the latest released PG? Regarding company-coq: no idea. Which features are you interested in?

spitters commented 8 years ago

Following the instructions in the easycrypt README line 256.

emacs, PG installed from ubuntu 15.04. GNU Emacs 24.4.1 Version 4.3pre131011.

I've edited the proof general system wide installation in: /usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el

toke the proofgeneral/easycrypt/ directory from here: https://github.com/EasyCrypt/easycrypt

and put them here. /usr/share/emacs/site-lisp/proofgeneral

I've also updated my .emacs

Regarding company-coq, my guess is that most of the features from your screen shots are useful for easycrypt too.

cpitclaudel commented 8 years ago

Did these instructions work before? I have no experience with installing PG globally, so I don't think I can help much here.

cpitclaudel commented 8 years ago

Regarding company-coq: I don't really know what easycrypt is, so I don't know how we could support completion there, and that's really company-coq's main feature. I can try to help adjusting and porting trhings if someone is motivated to do the programming, but I don't currently have time to work on a port myself.

spitters commented 8 years ago

They seem to work on a mac and given that they are there, I am assuming that they work for others too. I am waiting for a response from the easycrypt mailing list.

On Wed, Jan 27, 2016 at 11:07 PM, Clément Pit--Claudel < notifications@github.com> wrote:

Did these instructions work before? I have no experience with installing PG globally, so I don't think I can help much here.

— Reply to this email directly or view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-175885088.

strub commented 8 years ago

Hi. I will create a pull request in a few. That should easy the distribution of PG with EC support.

Regarding company, I can provide the necessary support for completion. Now, I would really prefer to first have your latex mode, as presented at CoqPL.

cpitclaudel commented 8 years ago

I'd love to see the LaTeX stuff happen, but it will require support from Coq :) Thanks for the PR.

strub commented 8 years ago

I was speaking about having this for EasyCrypt. If you explain me how this can be included in the EasyCrypt portion of PG, I can quickly add the "printing only" notations into EasyCrypt.

cpitclaudel commented 8 years ago

Ah, cool! But I'm not sure what the right approach is (hence my launching the discussion on coqdev). At a high level, I guess what one would need is two things: delimiters for LaTeX math (to tell Emacs: TeXify stuff from here to there), and support for getting proper LaTeX notations between these delimiters. After this support should be reasonably easy to implement in Emacs (but I'm not sure how much time I'll have in the next few weeks)

Matafou commented 8 years ago

Hi,

What is the current status of easycrypt/PG? I don't see an easycrypt directory.

Potentially easycrypt is the only "other" prover other than coq with a recent explicit intention to use PG.

There currently ongoing work to switch coq/pg to a new protocol between coq and pg, abd it may have consequencies on easycrypt support on PG.

Hence my question. Is it still the case that there is ap lan to have an easycrypt/PG? In this case we have to be careful.

psteckler commented 8 years ago

My changes to PG won't allow any other provers to run, because the proof shell code is being removed.

I had originally planned to leave in the proof shell code, and allow "dual-mode" operation. The plan changed to make PG Coq-only.

-- Paul

On Fri, Jul 22, 2016 at 11:14 AM, Pierre Courtieu notifications@github.com wrote:

Hi,

What is the current status of easycrypt/PG? I don't see an easycrypt directory.

Potentially easycrypt is the only "other" prover other than coq with a recent explicit intention to use PG.

There currently ongoing work to switch coq/pg to a new protocol between coq and pg, abd it may have consequencies on easycrypt support on PG.

Hence my question. Is it still the case that there is ap lan to have an easycrypt/PG? In this case we have to be careful.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-234571444, or mute the thread https://github.com/notifications/unsubscribe-auth/ACJAKFGjfw4DwmR7wCRrmbSuvMYPMuhbks5qYN5ZgaJpZM4HNyyE .

cpitclaudel commented 8 years ago

I don't expect this to be an issue in the easycrypt case: it's still possible to base it on the tagged version of PG before moving to Coq's protocol.

Matafou commented 8 years ago

Sure, but some part of the future development of pg could benefit to easycrypt.

Well, I guess the fork can still cherry-pick for some time...

P.

2016-07-22 17:29 GMT+02:00 Clément Pit--Claudel notifications@github.com:

I don't expect this to be an issue in the easycrypt case: it's still possible to base it on the tagged version of PG before moving to Coq's protocol.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-234575449, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6h9B-_DPvUGQbppHAvpZY6IQBMsVks5qYOHTgaJpZM4HNyyE .

cpitclaudel commented 8 years ago

Yup; I talked about it with Emilio. My expectation is that once we migrate to SerAPI, we'll be able to have add a wrapper around REPLs that exposes the SerAPI interface, but uses a REPL under the hood.

In other words, even without changes on the easycrypt side, I think we'll be able to support it in the new PG once we move to SerAPI.

Matafou commented 8 years ago

OK, we will see. Thanks.

2016-07-22 17:50 GMT+02:00 Clément Pit--Claudel notifications@github.com:

Yup; I talked about it with Emilio. My expectation is that once we migrate to SerAPI, we'll be able to have add a wrapper around REPLs that exposes the SerAPI interface, but uses a REPL under the hood.

In other words, even without changes on the easycrypt side, I think we'll be able to support it in the new PG once we move to SerAPI.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-234581099, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6oLsy2HncapnUHlpcppjIN8U5FWRks5qYOa4gaJpZM4HNyyE .

strub commented 8 years ago

I've been a bit lazy with the admin. stuff, but this is still in the line.

I don't understand what it means to "stop the support for other provers". Does it mean that proof general only accepts provers whose logic only accepts models that need the existence of a strictly monotonous chain of non-accessible cardinals, or that other provers have to move to a different protocol? For the latter, i don't mind adapting EasyCrypt s.t. we can benefit from the new PG. If PG is going to be really Coq specific (i.e. that specific that EasyCrypt cannot be adapted to work with it), i find this very disappointing.

psteckler commented 8 years ago

Until now, PG required that provers use a REPL. Configuring PG for a prover meant mostly writing regexps to recognize the output of the REPL.

Since 8.5, Coq has supported a wire protocol with SGML/XML tags to wrap data. That's what CoqIDE uses. The main benefit of the wire protocol is that it allows asynchronous processing of individual theorems/lemmas, which can speed things up on a multi-core machine.

We decided that we would support the wire protocol in PG to gain that benefit. That mode of operation is wholly unlike interacting with a REPL, and we chose to abandon that part of PG. The impression I had was that PG had become de facto Coq-only, so there would not be serious consequence.

In fact, the way the code is structured in my branch would allow support for other provers, if they have a wire protocol available. Is that the case for EasyCrypt?

-- Paul

On Fri, Jul 22, 2016 at 4:42 PM, Pierre-Yves Strub <notifications@github.com

wrote:

I've been a bit lazy with the admin. stuff, but this is still in the line.

I don't understand what it means to "stop the support for other provers". Does it mean that proof general only accepts provers whose logic only accepts models that need the existence of a strictly monotonous chain of non-accessible cardinals, or that other provers have to move to a different protocol? For the latter, i don't mind adapting EasyCrypt s.t. we can benefit from the new PG. If PG is going to be really Coq specific (i.e. that specific that EasyCrypt cannot be adapted to work with it), i find this very disappointing.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-234651061, or mute the thread https://github.com/notifications/unsubscribe-auth/ACJAKDkfcHA7prthsDbr_I4UPKkyzQzGks5qYSs6gaJpZM4HNyyE .

strub commented 8 years ago

Is this protocol documented somewhere? To say, the REPL protocol is kind of hacky and i would prefer to move to a more structured one. Since EasyCrypt does not have such protocol currently, i would go for it instead of inventing my own one.

psteckler commented 8 years ago

Well, the SGML/XML protocol is based on the use of states in Coq, the so-called STM, that would not carry over to another prover, I think, unless it chose to implement something similar internally. There's some documentation for it available through Coqtop's command-line help, though it's far from complete.

Further, the plan is to switch over eventually to another wire protocol, SerAPI, that uses the same STM, but offers some benefits. We're using the SGML/XML protocol for now, because SerAPI is still under development, and we'd like to get something out the door.

If EasyCrypt wants to use its own wire protocol, I can make it so that PG will allow using other protocol handlers. The code is sort of structured that way now, but I was about to embark on code simplification that might otherwise close off that avenue.

-- Paul

On Fri, Jul 22, 2016 at 5:07 PM, Pierre-Yves Strub <notifications@github.com

wrote:

Is this protocol documented somewhere? To say, the REPL protocol is kind of hacky and i would prefer to move to a more structured one. Since EasyCrypt does not have such protocol currently, i would go for it instead of inventing my own one.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-234656899, or mute the thread https://github.com/notifications/unsubscribe-auth/ACJAKJRSyIpGbQdSHPvvGpOYV69x6srxks5qYTD4gaJpZM4HNyyE .

strub commented 8 years ago

I would prefer PG to allow such third party protocol handlers. I'm not planing to maintain a mode for a dead & staled PG version. Are you in the Paris area (I see that you're participating to Coq's GTs). If so, maybe can we meet this fall s.t. you explain to me how to implement such handlers.

cpitclaudel commented 8 years ago

Hey @strub,

A slightly higher-level answer:

What we're doing is reworking PG's internals to remove the assumption that it's talking to a REPL. For historical and code organization reasons, this is hard, so as a first step we're doing this for Coq. We have no plan to make PG coq-specific; that is, we have no desire to integrate so closely that it wouldn't work with other provers. In particular, there's no reason why EasyCrypt couldn't work with PG in the future.

The protocol that we're implementing for Coq is far from nice; you don't want to waste time implementing that. I've been talking with Valentin (PeaCoq) and Emilio (jsCoq) about a cleaner, simpler protocol. Emilio is developing it (SerAPI), and when I saw him last month we talked about EasyCrypt as well. I think, and so does he, that it should be easy to support that protocol in EasyCrypt; see https://github.com/ejgallego/coq-serapi/ .

Once things have stabilized a bit, we'll move PG to that cleaner protocol. At that point, we'll be able to connect PG to EasyCrypt again.

In the meantime, we'll have a REPL branch; EasyCrypt will be usable with that branch, as before :) If there's demand on the EasyCrypt side, it shouldn't be hard to cherry-pick bug-fixes made on master to apply them to the REPL branch.

Does that make sense?

cpitclaudel commented 8 years ago

@strub Do you have time for a quick Skype call in the next few days, btw? I'm at CAV atm, but I should be available on Sunday.

psteckler commented 8 years ago

No, I'm in the US (I may be in France at some point).

The code I have so far (still needs lots of cleanup) is at:

https://github.com/psteckler/ProofGeneral

branch "server-protocol".

I'm happy to work with you to accomodate another protocol.

-- Paul

On Fri, Jul 22, 2016 at 5:33 PM, Pierre-Yves Strub <notifications@github.com

wrote:

I would prefer PG to allow such third party protocol handlers. I'm not planing to maintain a mode for a dead & staled PG version. Are you in the Paris area (I see that you're participating to Coq's GTs). If so, maybe can we meet this fall s.t. you explain to me how to implement such handlers.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/43#issuecomment-234662448, or mute the thread https://github.com/notifications/unsubscribe-auth/ACJAKLuc6wyQRdg5vAOHkot8H6SQ9Bqmks5qYTc3gaJpZM4HNyyE .

cpitclaudel commented 8 years ago

I would prefer PG to allow such third party protocol handlers. I'm not planing to maintain a mode for a dead & staled PG version.

Of course; the only question is whether we put the complexity of third party protocols in PG, or we require provers to expose a semi-unified interface, and possibly write adapters when provers don't obey that interface. For example, once we have SerAPI, it'll be easy to support REPLs again by adding a REPL → SerAPI wrapper.

strub commented 8 years ago

@cpitclaudel This makes sense. I just wanted to be sure that EasyCrypt won't be pruned out from PG. So, to sum up:

Do you have an idea of how long this will take before PG moves to SetAPI. Also, i can do a Skype, starting from Tuesday.

cpitclaudel commented 8 years ago

Do you have an idea of how long this will take before PG moves to SetAPI.

Not entirely clear: we haven't even moved to the other API yet :)

Also, i can do a Skype, starting from Tuesday.

Awesome. I'll write you an email.

spitters commented 7 years ago

For posterity, trying to remember what fixed the issue for me. I believe my issue was solved by using the github version of PG, instead of the one in ubuntu.

hendriktews commented 7 years ago

From the last comment I conclude that this issue has been fixed.

remysucre commented 7 years ago

@strub any news on company-coq for EC?