Stream: Beginner Questions

Topic: very new to isabelle, can't open WasmCert


view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 16:30):

why is everything in red? and why is everything 'pending'? pending.png

this is the repo i'm trying to open btw https://github.com/WasmCert/WasmCert-Isabelle

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 16:36):

hmm the interface is extremely confusing but anyway how can i resolve this error then? Screenshot-from-2021-06-24-23.35.24.png

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 16:36):

it says bad theory import

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 16:36):

and i have no idea how to fix it

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 16:36):

can i like 'download' the theory somewhere

view this post on Zulip Manuel Eberl (Jun 24 2021 at 16:41):

You should download and install the AFP: https://www.isa-afp.org/download.html

Information on how to install it here: https://www.isa-afp.org/using.html

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 16:51):

the error still persists even after installing the AFP. did i install it wrong?

ubuntu@resourceful-man:~$ wget https://www.isa-afp.org/release/afp-current.tar.gz
--2021-06-24 16:43:13--  https://www.isa-afp.org/release/afp-current.tar.gz
Resolving www.isa-afp.org (www.isa-afp.org)... 131.159.47.3
Connecting to www.isa-afp.org (www.isa-afp.org)|131.159.47.3|:443... connected.
HTTP request sent, awaiting response... 200 OK
Length: 76657222 (73M) [application/x-gzip]
Saving to: ‘afp-current.tar.gz’

afp-current.tar.gz            100%[================================================>]  73.11M  2.17MB/s    in 29s

2021-06-24 16:43:49 (2.51 MB/s) - ‘afp-current.tar.gz’ saved [76657222/76657222]

ubuntu@resourceful-man:~$ isabelle
isabelle: command not found
ubuntu@resourceful-man:~$ ./Isabelle2021/
Isabelle2021  bin/          contrib/      doc/          etc/          heaps/        lib/          src/
ubuntu@resourceful-man:~$ ./Isabelle2021/bin/isabelle components -u
/home/ubuntu/Isabelle2021/lib/Tools/components: option requires an argument -- u

Usage: isabelle components [OPTIONS] [COMPONENTS ...]

  Options are:
    -I           init user settings
    -R URL       component repository (default $ISABELLE_COMPONENT_REPOSITORY)
    -a           resolve all missing components
    -l           list status
    -u DIR       update $ISABELLE_HOME_USER/components: add directory
    -x DIR       update $ISABELLE_HOME_USER/components: remove directory

  Resolve Isabelle components via download and installation: given COMPONENTS
  are identified via base name. Further operations manage etc/settings and
  etc/components in $ISABELLE_HOME_USER.

  ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components"
  ISABELLE_HOME_USER="/home/ubuntu/.isabelle/Isabelle2021"

ubuntu@resourceful-man:~$ tar -xf afp-current.tar.gz
ubuntu@resourceful-man:~$ ./Isabelle2021/bin/isabelle components -u afp-
afp-2021-06-23/     afp-current.tar.gz
ubuntu@resourceful-man:~$ ./Isabelle2021/bin/isabelle components -u afp-2021-06-23/
Added component "/home/ubuntu/afp-2021-06-23"

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 17:08):

lol i didn't read the instructions carefully...

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 17:08):

i had to run ./Isabelle2021/bin/isabelle components -u afp-2021-06-23/thys

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 17:08):

wow

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 17:08):

sorry for bothering all of you

view this post on Zulip Huỳnh Trần Khanh (Jun 24 2021 at 17:08):

thanks lol

view this post on Zulip Manuel Eberl (Jun 24 2021 at 17:17):

No worries!


Last updated: Sep 25 2021 at 08:21 UTC