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?
THANK YOU VERY MUCH!