easycrypt

[proofgeneral]

easycrypt

[cpitclaudel]

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

[spitters]

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]

@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]

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]

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

[cpitclaudel]

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]

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 <
[email protected]> 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
#43 (comment).

[strub]

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]

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

[strub]

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]

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]

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]

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 [email protected]
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
#43 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/ACJAKFGjfw4DwmR7wCRrmbSuvMYPMuhbks5qYN5ZgaJpZM4HNyyE
.

[cpitclaudel]

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]

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 [email protected]:

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
#43 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/AEsl6h9B-_DPvUGQbppHAvpZY6IQBMsVks5qYOHTgaJpZM4HNyyE
.

[cpitclaudel]

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]

OK, we will see. Thanks.

2016-07-22 17:50 GMT+02:00 Clément Pit--Claudel [email protected]:

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
#43 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/AEsl6oLsy2HncapnUHlpcppjIN8U5FWRks5qYOa4gaJpZM4HNyyE
.

[strub]

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]

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 <[email protected]

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
#43 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/ACJAKDkfcHA7prthsDbr_I4UPKkyzQzGks5qYSs6gaJpZM4HNyyE
.

[strub]

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]

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 <[email protected]

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
#43 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/ACJAKJRSyIpGbQdSHPvvGpOYV69x6srxks5qYTD4gaJpZM4HNyyE
.

[strub]

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]

Hey @strub,

A slightly higher-level answer:

• PG's architecture has not evolved very much in the last many years, but the way people use theorem provers has. We're trying to modernize PG, and a good occasion to do this is that Coq has a new async protocol. In particular, moving away from the REPL model would be nice. This way we could, e.g., support Isabelle again. This is in part in the line of the old PGIP work.
• Currently, Coq and EasyCrypt are PG's two only in-use clients, and Coq's the only "official" one, though we'd love to merge EasyCrypt support in.

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]

@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]

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 <[email protected]

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
#43 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/ACJAKLuc6wyQRdg5vAOHkot8H6SQ9Bqmks5qYTc3gaJpZM4HNyyE
.

[cpitclaudel]

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]

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

• EasyCrypt continues with REPL and an old version of PG, but
• when SerAPI stabilises, PG will move to it & it will be sufficient for EasyCrypt to move to that protocol.

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]

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]

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]

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

[remysucre]

@strub any news on company-coq for EC?