zibo yang (May 25 2021 at 19:25): zibo yang (May 25 2021 at 19:25):when I wanted to refer to AFP, I followed the instruction for windows with command "isabelle components -u /cygdrive/c/afp-current/afp-2021-05-14" and I saw "added components", but my Isabelle still cannot identify any file in AFP. why it happens?
Jakub Kądziołka (May 25 2021 at 19:28):what do you mean by "my Isabelle still cannot identify any file in AFP"? Also, did you restart jEdit after adding the component?
zibo yang (May 25 2021 at 19:29):yes I restart it but it doesn't work
zibo yang (May 25 2021 at 19:29):now I am trying to reinstall isabelle and see if it works
Jakub Kądziołka (May 25 2021 at 19:30):define "doesn't work"
Jakub Kądziołka (May 25 2021 at 19:30):what are the actions you're performing to determine that
zibo yang (May 25 2021 at 19:31):it shows like "Bad theory Real_Roots"
Jakub Kądziołka (May 25 2021 at 19:31):what code does that happen on?
zibo yang (May 25 2021 at 19:41):ok it still doesn't work
Jakub Kądziołka (May 25 2021 at 19:41):Jakub Kądziołka said:
what code does that happen on?
zibo yang (May 25 2021 at 19:42):If I try to code:
theory Scratch
imports Real_Roots
begin
end
it shows:
Bad theory import "Draft.Real_Roots"
which AFP entry's Real_Roots do you want?
zibo yang (May 25 2021 at 19:43):I want to refer to Real_Roots.thy in AFP
Jakub Kądziołka (May 25 2021 at 19:50):then write imports Algebraic_Numbers.Real_Roots
zibo yang (May 25 2021 at 19:52):Jakub Kądziołka said:
then write
imports Algebraic_Numbers.Real_Roots
it doesn't work, too.
Simon Roßkopf (May 25 2021 at 20:01):Does it still show the same error message?
zibo yang (May 25 2021 at 20:02):Simon Roßkopf said:
Does it still show the same error message?
yes
Simon Roßkopf (May 25 2021 at 20:07):Does the error message persist after leaving jEdit opened for a few seconds/minutes?
Algebraic_Numbers.Real_Roots depends on quite a lot of material, for which Isabelle has to resolve the dependencies first. Loading all of it directly from the default HOL heap image can take a lot of time.
Jakub Kądziołka (May 25 2021 at 20:08):see if there's any activity in the Theories tab (hidden button on the right by default)
zibo yang (May 25 2021 at 20:20):Simon Roßkopf said:
Does the error message persist after leaving jEdit opened for a few seconds/minutes?
Algebraic_Numbers.Real_Rootsdepends on quite a lot of material, for which Isabelle has to resolve the dependencies first. Loading all of it directly from the default HOL heap image can take a lot of time.
For my current file, the JVM and ML doesn't change and error is still there. But I encountered some other weird phenomenon: In another file"Euclidean_Space.thy", the theory "Topological_Space" took a while to disappear and finally it works. But in my current file, "Topological_Space" still triggers the error and JVM doesn't change.......
zibo yang (May 25 2021 at 20:28):By the way, where should I open terminal and tap the command "isabelle components -u /home/myself/afp" if I want to refer to AFP with linux
Jakub Kądziołka (May 25 2021 at 20:29):your $PWD doesn't matter
zibo yang (May 25 2021 at 20:32):Jakub Kądziołka said:
your
$PWDdoesn't matter
but it indicates:
~/Desktop/Isabelle2021_linux/Isabelle2021$ isabelle components -u /home/afp-current
Traceback (most recent call last):
File "/usr/lib/command-not-found", line 28, in <module>
from CommandNotFound import CommandNotFound
File "/usr/lib/python3/dist-packages/CommandNotFound/CommandNotFound.py", line 19, in <module>
from CommandNotFound.db.db import SqliteDatabase
File "/usr/lib/python3/dist-packages/CommandNotFound/db/db.py", line 5, in <module>
import apt_pkg
ModuleNotFoundError: No module named 'apt_pkg'
that's an error generated by the program installed by your operating system to generate nicer error messages than command not found
Jakub Kądziołka (May 25 2021 at 20:38):if isabelle is not in $PATH, you'll need to use ./isabelle
zibo yang (May 25 2021 at 20:42):Jakub Kądziołka said:
if isabelle is not in
$PATH, you'll need to use./isabelle
sorry I don't get a point about how this command looks like?
Jakub Kądziołka (May 25 2021 at 20:45):in the Isabelle2021 folder, ./bin/isabelle components -u /path/to/afp
zibo yang (May 25 2021 at 20:46):~/Desktop/Isabelle2021_linux/Isabelle2021/contrib$ ./bin/isabelle components -u /home/afp-current/afp-2021-04-09
bash: ./bin/isabelle: No such file or directory
I've explicitly said where you're supposed to be, and you're surprised that the command doesn't work somewhere else
zibo yang (May 25 2021 at 20:56):Jakub Kądziołka said:
I've explicitly said where you're supposed to be, and you're surprised that the command doesn't work somewhere else
? this command runs in Isabelle 2021 folder.
Jakub Kądziołka (May 25 2021 at 20:56):no, you're in Isabelle2021/contrib
zibo yang (May 25 2021 at 20:58):sorry my fault
zibo yang (May 25 2021 at 21:04):Ok it shows "added components", but it still doesn't work if I code "Algebraic_Numbers.Real_Roots" and get some error
Jakub Kądziołka (May 25 2021 at 21:05):"some error"?
zibo yang (May 25 2021 at 21:06):sorry same error
Jakub Kądziołka (May 25 2021 at 21:06):click on the "theories" button on the right side of your screen. what do you see?
zibo yang (May 25 2021 at 21:10):sorry I cannot see theory button in my linux isabelle, but I can see it in my windows isabelle
Jakub Kądziołka (May 25 2021 at 21:14):Go to Plugins > Isabelle > Theories panel in the menu at the top
zibo yang (May 25 2021 at 21:17):ok the only thing I can see is one rectangle of Scratch
Jakub Kądziołka (May 25 2021 at 21:18):what does the command cat ~/.isabelle/Isabelle2021/etc/components say?
zibo yang (May 25 2021 at 21:21):ziboyang@ziboyang-virtual-machine:~/Desktop/Isabelle2021_linux/Isabelle2021$ cat ~/.isabelle/Isabelle2021/etc/components
/home/ziboyang/afp-current/afp-2021-04-09
okay, what does ls /home/ziboyang/afp-current/afp-2021-04-09/ROOTS say?
zibo yang (May 25 2021 at 21:22):ziboyang@ziboyang-virtual-machine:~/Desktop/Isabelle2021_linux/Isabelle2021$ ls /home/ziboyang/afp-current/afp-2021-04-09/ROOTS
ls: cannot access '/home/ziboyang/afp-current/afp-2021-04-09/ROOTS': No such file or directory
hmm. Looks like there's a problem with the instructions – they've been updated semi-recently. Try
./bin/isabelle components -x ~/afp-current/afp-2021-04-09
./bin/isabelle components -u ~/afp-current/afp-2021-04-09/thys
ziboyang@ziboyang-virtual-machine:~/Desktop/Isabelle2021_linux/Isabelle2021$ ./bin/isabelle components -x ~/afp-current/afp-2021-04-09
Removed component "/home/ziboyang/afp-current/afp-2021-04-09"
ziboyang@ziboyang-virtual-machine:~/Desktop/Isabelle2021_linux/Isabelle2021$ ./bin/isabelle components -u ~/afp-current/afp-2021-04-09/thys
*** Bad component directory: "/home/ziboyang/afp-current/afp-2021-04-09/thys"
huh, ls ~/afp-current/afp-2021-04-09/ | head?
zibo yang (May 25 2021 at 21:29):ziboyang@ziboyang-virtual-machine:~/Desktop/Isabelle2021_linux/Isabelle2021$ ls ~/afp-current/afp-2021-04-09/ | head
etc
thys
tools
Okay, I have reproduced your problems on my side. This should make things work:
echo "/home/ziboyang/afp-current/afp-2021-04-09/thys" > ~/.isabelle/Isabelle2021/etc/components
I'll send a mail to the ML summarizing the problem
Jakub Kądziołka (May 25 2021 at 21:37):Let me know whether it works
zibo yang (May 25 2021 at 21:48):Here is another weird problem occurs with my first line"theory Scratch":
Outer syntax error⌂: command expected,
but identifier Theory⌂ was found
oh the problem is still there
zibo yang (May 25 2021 at 22:11):Ok I think that it maybe works since I saw that there is "Algebraic_Numbers. Real_Roots" occurs in the prompt when I tap "Real_" . But another problems is that my IDE in linux always collapses and disappears during its computation so that I cannot see if the IDE really identify "Real_Roots". Do you have any suggestion about that?
zibo yang (May 25 2021 at 22:13):And I guess my windows Isabelle IDE shares the same problem with linux one. How to address that problem with Windows version
zibo yang (May 26 2021 at 08:54):Sorry is there anyone to help me about this problem above?
Jakub Kądziołka (May 26 2021 at 10:51):open $ISABELLE_HOME_USER/etc/components in Isabelle/jEdit (it should work when you paste the path) and append /thys to the line with the path to your AFP
Jakub Kądziołka (May 26 2021 at 10:51):zibo yang said:
Ok I think that it maybe works since I saw that there is "Algebraic_Numbers. Real_Roots" occurs in the prompt when I tap "Real_" . But another problems is that my IDE in linux always collapses and disappears during its computation so that I cannot see if the IDE really identify "Real_Roots". Do you have any suggestion about that?
This might be caused by an out-of-memory condition.
zibo yang (May 26 2021 at 11:37):Jakub Kądziołka said:
open
$ISABELLE_HOME_USER/etc/componentsin Isabelle/jEdit (it should work when you paste the path) and append/thysto the line with the path to your AFP
Thanks a lot. It finally works on my windows version. :+1: I am sorry to bother you yesterday so late
Last updated: Dec 21 2024 at 16:20 UTC