Can't find nun-file after using nunchaku in isabelle

nunchaku-inria / nunchaku

Model finder for higher-order logic

https://nunchaku-inria.github.io/nunchaku/

BSD 2-Clause "Simplified" License

42 stars 3 forks source link

Can't find nun-file after using nunchaku in isabelle #33

Open singhjagadish opened 5 years ago

singhjagadish commented 5 years ago

Hello,

I have used nunchaku on an isabelle lemma, and I get an error because of an ill-formed term (probably caused by using an own datatype, more specifically a domain). It also shows the directory where the .nun-file (nunchaku2832584.nun) of the process should be. However, I couldn't find the file there, so my question is how to get the information of the file, as it could be helpful for using nunchaku for such a datatype.

Thanks in advance.

c-cube commented 5 years ago

The nunchaku plugin is Isabelle isn't production ready yet, sorry. @blanchette would probably know more but he's quite busy these days.