Yijun He (Jul 17 2019 at 09:44): Yijun He (Jul 17 2019 at 09:44):My Isabelle sometimes gives an error when the proof method smt is used. The error message is usually like this: exception Io {cause = SysErr ("The system cannot find the path specified.", SOME ERROR_PATH_NOT_FOUND), function = "BinIO.openOut", name = "C:\\Users\\Micha\\AppData\\Local\\Temp\\isabelle-Micha\\process6803350045593986926\\cache-io-4230284"} raised (line 124 of "./basis/BinIO.sml"), and I have to restart Isabelle every time this happens. Does anyone also have this problem, or is it just specific to my computer? (I actually bought a new laptop recently, but this problem happens on both my old laptop and the new one) Many thanks!
Hanna Lachnitt (Jul 17 2019 at 09:50):I have never encountered that :/ But I am using Linux it might be something Windows specific.
Yijun He (Jul 17 2019 at 09:52):Then that might be a system-specific error? Windows 10 often have some weird bugs.
Anthony Bordg (Jul 17 2019 at 10:27):@Yijun He I vaguely remember that someone (@Lawrence Paulson ?) told me there are well known problems with smt and some computers (maybe that person even mentioned that it's related to the OS used and in particular Windows).
Moreover, note that the use of smt should be avoided whenever possible (it's not forbidden though). Please see this guide (third bullet in the section Good Reasons).
Yijun He (Jul 17 2019 at 10:30):Got it. Then I will try to use less smt in my proofs.
Last updated: Apr 25 2024 at 04:18 UTC