search

ProofGeneral / PG

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

easycrypt example #146

Open hendriktews opened 7 years ago

hendriktews commented 7 years ago

@strub Could you add a little easycrypt example, such that one could try your easycrypt mode?

spitters commented 7 years ago

Thanks for the nice easycrypt support! It works very well. However, there are a few glitches in the indentation support. Here is an example:

lemma test: true.
    proof.
      trivial.
    qed.

There should be no indentation before proof. There are more indentation glitches and I think they are easy to find with some basic editing. Please let me know if you need more info.

Matafou commented 7 years ago

Hi, Indentation is not generically supported by proofgeneral. You need to implement it by yourself.

If the syntax is simple I may try to provide a starting point using the smie library like for coq.

Can you provide a informal grammar and/or some file with samples covering the whole syntax?

P.

spitters commented 7 years ago

@strub or @fdupress would be the ones most knowledgeable I guess. Meanwhile I was happy to find out that M-x electric-indent-mode disables it :-)

Thanks for the PG, in any case.

strub commented 7 years ago

I can provide a file with all the idiomatic construction. I think that Coq already have isomorphic constructions :)

Matafou commented 7 years ago

Hopefully easycrypt is not isomorphic to the terrible overloading of tenth of symbols of coq...

Think about what indentation in coq has to do when meeting a line starting with "with" for instance. Even "." is overloaded.