-
Notifications
You must be signed in to change notification settings - Fork 85
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
easycrypt #43
Comments
Sure, that would be good :) Do you want to prepare a pull request? |
Currently, PG + easycrypt does not install for me. I am following the system wide installation instructions. 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? |
@spitters Can you clarify how you installed PG? Does that procedure work with the latest released PG? |
Following the instructions in the easycrypt README line 256. emacs, PG installed from ubuntu 15.04. I've edited the proof general system wide installation in: toke the proofgeneral/easycrypt/ directory from here: and put them here. 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. |
Did these instructions work before? I have no experience with installing PG globally, so I don't think I can help much here. |
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. |
They seem to work on a mac and given that they are there, I am assuming On Wed, Jan 27, 2016 at 11:07 PM, Clément Pit--Claudel <
|
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. |
I'd love to see the LaTeX stuff happen, but it will require support from Coq :) Thanks for the PR. |
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. |
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) |
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. |
My changes to PG won't allow any other provers to run, because the proof I had originally planned to leave in the proof shell code, and allow -- Paul On Fri, Jul 22, 2016 at 11:14 AM, Pierre Courtieu 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. |
Sure, but some part of the future development of pg could benefit to 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:
|
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. |
OK, we will see. Thanks. 2016-07-22 17:50 GMT+02:00 Clément Pit--Claudel notifications@github.com:
|
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. |
Until now, PG required that provers use a REPL. Configuring PG for a prover Since 8.5, Coq has supported a wire protocol with SGML/XML tags to wrap We decided that we would support the wire protocol in PG to gain that In fact, the way the code is structured in my branch would allow support -- Paul On Fri, Jul 22, 2016 at 4:42 PM, Pierre-Yves Strub <notifications@github.com
|
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. |
Well, the SGML/XML protocol is based on the use of states in Coq, the Further, the plan is to switch over eventually to another wire protocol, If EasyCrypt wants to use its own wire protocol, I can make it so that PG -- Paul On Fri, Jul 22, 2016 at 5:07 PM, Pierre-Yves Strub <notifications@github.com
|
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. |
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? |
@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. |
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
|
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. |
@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. |
Not entirely clear: we haven't even moved to the other API yet :)
Awesome. I'll write you an email. |
For posterity, trying to remember what fixed the issue for me. |
From the last comment I conclude that this issue has been fixed. |
@strub any news on company-coq for EC? |
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.
The text was updated successfully, but these errors were encountered: