Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Jedit error


view this post on Zulip Email Gateway (Dec 23 2021 at 10:51):

From: Peyman Derafsh Kavian <peymankavian@gmail.com>
Good day

I have been trying to compile a theory file from a tool but getting a
weird error. I paste it below:

$ isabelle jedit -d . -l HOL-TestGen "examples/unit/List/List_test.thy"
5:40:40 PM [main] [error] main: java.io.FileNotFoundException:
C:\Users\Peyman\.isabelle\Isabelle2016-1\jedit\activity.log (Access is
denied)
5:40:40 PM [main] [error] main: at java.io.FileOutputStream.open0(Native
Method)
5:40:40 PM [main] [error] main: at
java.io.FileOutputStream.open(FileOutputStream.java:270)
5:40:40 PM [main] [error] main: at
java.io.FileOutputStream.<init>(FileOutputStream.java:213)
5:40:40 PM [main] [error] main: at
java.io.FileOutputStream.<init>(FileOutputStream.java:101)
5:40:40 PM [main] [error] main: at
java.io.FileWriter.<init>(FileWriter.java:63)
5:40:40 PM [main] [error] main: at
org.gjt.sp.jedit.jEdit.main(jEdit.java:417)
5:40:40 PM [main] [error] main: at
sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
5:40:40 PM [main] [error] main: at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
5:40:40 PM [main] [error] main: at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
5:40:40 PM [main] [error] main: at
java.lang.reflect.Method.invoke(Method.java:498)
5:40:40 PM [main] [error] main: at
isabelle.Main$$anonfun$2.apply(main.scala:81)
5:40:40 PM [main] [error] main: at isabelle.Main$.main(main.scala:91)
5:40:40 PM [main] [error] main: at isabelle.Main.main(main.scala)

Could I get some advice for that? Thank you in advance.

Regards,
Peyman Kavian

view this post on Zulip Email Gateway (Dec 23 2021 at 11:16):

From: Makarius <makarius@sketis.net>
Isabelle2016-1 is from December 2016: 5 years ago. Many things can go wrong
from the historic distance: the surrounding operating system diverges and
implicit assumptions no longer hold. Windows is especially critical here,
because it often needs special workarounds that change over time.

If you do need such an old Isabelle version for HOL-TestGen, I recommend to
use it with a clean Linux installation from that time, e.g. Ubuntu 16.04 or
18.04 (but newer versions might accidentally work as well).

Another side remark: the terminology to "compile a theory file" is very
strange. The process of checking formal sources and assign a meaning is more
like an interpretation. It is better to say to "check a theory file" (thinking
of specifications and proofs) or more generically to "process a theory file"
(thinking also of add-on things beyond specifications and proofs).

Makarius

view this post on Zulip Email Gateway (Dec 23 2021 at 14:06):

From: y.nemouchi@ensbiotech.edu.dz
Dear Peyman Kavian,

I have cced the main developers, they might be able to help you.
However, please next time change topic name from "Jedi-t error" to
"HOL-TestGen-jedit error" or something in those lines.

@Achim/Burkhart: Someone needs help with HOL-Testgen build in Isabelle
mailing list.

Best wishes,

Yakoub.


Last updated: Jul 15 2022 at 23:21 UTC