I am working on compiling Ynot library (8.3pl2 Release). My idea is just to follow its Tutorial to get a sense of how it turns Coq to be non-terminated and have side effects. Then, I would like to re-implement the certified web services with Ynot. This idea is from the paper called “Certified Web Services in Ynot”.
I have problems compiling the Ynot library. Since this project was created more than ten years ago, some tactics are out-of-date. I suppose they used proof general to develop the system. However, I am now using CoqIDE. It’s clear that many issues will come up when compiling this project. I tried my best to modify the source code. However, I still have many problems.
I am asking whether some of you have experience with Ynot. Have you successfully compiled the Ynot in CoqIDE. If yes, will it be possible to share your modified project? Or would I get in touch with you to get help?
Second, you might need to make a lot of updates to the code.
Given that Ynot is 10+ years old, it would be based on a version of Coq prior to V7-0 (Nov 2013). See Releases · coq/coq · GitHub.
If it’s difficult to update the code, you might try installing older version(s) of Coq and getting the code to work on those older version(s) as an intermediate step. OTOH this may not be easy or not even helpful, either.
I agree in general, but the correct Coq version appears to be 8.3pl2 (as implied by the Ynot website, Release V8.3pl2 · coq/coq · GitHub). The porting is nevertheless going to be challenging.
Those tag dates are inaccurate; all tags until 8.4pl2 are dated Nov 18, 2013 (and described as “Restoring SVN tags”), but the underlying commits appear to have the correct dates; 8.3pl2 is from Apr 13, 2011;
while 7.0 is from 2001 (assuming that conversion worked better):