Stream: Beginner Questions

Topic: afp


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip zibo yang (May 25 2021 at 19:29):

yes I restart it but it doesn't work

view this post on Zulip zibo yang (May 25 2021 at 19:29):

now I am trying to reinstall isabelle and see if it works

view this post on Zulip Jakub Kądziołka (May 25 2021 at 19:30):

define "doesn't work"

view this post on Zulip Jakub Kądziołka (May 25 2021 at 19:30):

what are the actions you're performing to determine that

view this post on Zulip zibo yang (May 25 2021 at 19:31):

it shows like "Bad theory Real_Roots"

view this post on Zulip Jakub Kądziołka (May 25 2021 at 19:31):

what code does that happen on?

view this post on Zulip zibo yang (May 25 2021 at 19:41):

ok it still doesn't work

view this post on Zulip Jakub Kądziołka (May 25 2021 at 19:41):

Jakub Kądziołka said:

what code does that happen on?

view this post on Zulip 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"

view this post on Zulip Jakub Kądziołka (May 25 2021 at 19:43):

which AFP entry's Real_Roots do you want?

view this post on Zulip zibo yang (May 25 2021 at 19:43):

I want to refer to Real_Roots.thy in AFP

view this post on Zulip Jakub Kądziołka (May 25 2021 at 19:50):

then write imports Algebraic_Numbers.Real_Roots

view this post on Zulip 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.

view this post on Zulip Simon Roßkopf (May 25 2021 at 20:01):

Does it still show the same error message?

view this post on Zulip zibo yang (May 25 2021 at 20:02):

Simon Roßkopf said:

Does it still show the same error message?

yes

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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_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.

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.......

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 20:29):

your $PWD doesn't matter

view this post on Zulip zibo yang (May 25 2021 at 20:32):

Jakub Kądziołka said:

your $PWD doesn'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'

view this post on Zulip Jakub Kądziołka (May 25 2021 at 20:37):

that's an error generated by the program installed by your operating system to generate nicer error messages than command not found

view this post on Zulip Jakub Kądziołka (May 25 2021 at 20:38):

if isabelle is not in $PATH, you'll need to use ./isabelle

view this post on Zulip 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?

view this post on Zulip Jakub Kądziołka (May 25 2021 at 20:45):

in the Isabelle2021 folder, ./bin/isabelle components -u /path/to/afp

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 20:52):

I've explicitly said where you're supposed to be, and you're surprised that the command doesn't work somewhere else

view this post on Zulip 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.

view this post on Zulip Jakub Kądziołka (May 25 2021 at 20:56):

no, you're in Isabelle2021/contrib

view this post on Zulip zibo yang (May 25 2021 at 20:58):

sorry my fault

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:05):

"some error"?

view this post on Zulip zibo yang (May 25 2021 at 21:06):

sorry same error

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:14):

Go to Plugins > Isabelle > Theories panel in the menu at the top

view this post on Zulip zibo yang (May 25 2021 at 21:17):

ok the only thing I can see is one rectangle of Scratch

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:18):

what does the command cat ~/.isabelle/Isabelle2021/etc/components say?

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:21):

okay, what does ls /home/ziboyang/afp-current/afp-2021-04-09/ROOTS say?

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:25):

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

view this post on Zulip zibo yang (May 25 2021 at 21:27):

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"

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:28):

huh, ls ~/afp-current/afp-2021-04-09/ | head?

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:35):

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

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:36):

I'll send a mail to the ML summarizing the problem

view this post on Zulip Jakub Kądziołka (May 25 2021 at 21:37):

Let me know whether it works

view this post on Zulip 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

view this post on Zulip zibo yang (May 25 2021 at 21:53):

oh the problem is still there

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip zibo yang (May 26 2021 at 08:54):

Sorry is there anyone to help me about this problem above?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip zibo yang (May 26 2021 at 11:37):

Jakub Kądziołka said:

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

Thanks a lot. It finally works on my windows version. :+1: I am sorry to bother you yesterday so late


Last updated: Sep 25 2021 at 10:20 UTC