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

Getting Easycrypt to run on PG #354

Open AlyssaLytle opened 6 years ago

AlyssaLytle commented 6 years ago

I installed Easycrypt and ProofGeneral according to the instructions for my Mac, and when I click on a .ec file, it opens proof general, but when I try to step through the file, I get the error:

Starting: easycrypt -emacs -I /Users/abyrnes1/.opam/4.05.0/bin condition-case: Searching for program: No such file or directory, easycrypt

In customizations, I added the path to easycrypt in the load path, so I'm not sure why it isn't finding it.

jiawenliu commented 4 years ago

I have the same issue

erikmd commented 4 years ago

Hi @jiawenliu and @AlyssaByrnes, thanks for raising this issue! and sorry for late reply.

a few questions:

I added the path to easycrypt in the load path

the 'load-path is specific to loading .el files, not binaries.

You could try instead updating 'exec-path, namely:

M-: (add-to-list 'exec-path "/path/to/easycrypt/dir")

If this works, you could for example add this line in your .emacs.

Feel free to comment if this workarounds/fixes the issue or not.

ghost commented 4 years ago

Hi @erikmd . Thanks for your comment. I have the same issue. I've installed easy crypt as readme file on Mac OS. Could you please guide me how can I find the "/path/to/easycrypt/dir" ?