Anthony Bordg (Jul 03 2019 at 18:29): Anthony Bordg (Jul 03 2019 at 18:29):First, download and install Isabelle2019. Then, you should download the Archive of Formal Proofs and follow the instructions.
Last, a tip for a better and faster experience with Isabelle: you should probably build the HOL-Analysis library. After you opened Isabelle, check the HOL-Analysis library in the rightmost panel Theories, and finally close and reopen Isabelle. The HOL-Analysis library will be built.
Same process with any big library if you plan to use it heavily.
Anthony Bordg (Jul 04 2019 at 11:57):@Yijun He @Hanna Lachnitt is Isabelle2019 faster now ?
Yijun He (Jul 04 2019 at 12:01):Actually the prover failed last time when I was building the HOL-Analysis library, and I reverted back to the HOL library.
Anthony Bordg (Jul 04 2019 at 12:09):Actually the prover failed last time when I was building the HOL-Analysis library
Do you mean that Sledgehammer failed after you built the HOL-Analysis library and that the latter is directly linked with the former ?
Anthony Bordg (Jul 04 2019 at 12:15):@Yijun He Could it be that your CPU is not powerful enough ?
By the way, did you get a workstation at the lab ?
Yijun He (Jul 04 2019 at 12:17):Yijun He Could it be that your CPU is not powerful enough ?
By the way, did you get a workstation at the lab ?
Yes, my new computer's cpu is not very powerful. I still don't have the workstation yet.
Anthony Bordg (Jul 04 2019 at 12:20):@Yijun He Ok, I will get in touch with Larry about that.
Sebastian Sturm (Sep 20 2019 at 12:13):What is the recommended hardware to run Isabelle on. My Laptop has (only) 8G RAM and occasionally spents a lot of time in Garbage Collection. Sometimes it even swaps and the OS kills polyML. I can get hardware from my group, but it would be useful to know what is used in other groups
Kevin Kappelmann (Sep 20 2019 at 15:27):In simple terms: the more RAM (16GB+) and CPU power, the better.
Last updated: Apr 20 2024 at 12:26 UTC