Robert Soeldner (Aug 13 2021 at 13:29): Robert Soeldner (Aug 13 2021 at 13:29):I would like to use some published theories from the AFP. After downloading and extracting the afp-current.tar.gz package, I tried importing them using isabelle components -u /home/rsoeldner/repo/afp-2021-08-08/thys/ which fails with *** Bad component directory: "/home/rsoeldner/repo/afp-2021-08-08". I'm using Isabelle Isabelle2021: February 2021
Katharina Kreuzer (Aug 13 2021 at 13:46):I had a similar problem. Are you sure, the theorem files lie at /home/rsoeldner/repo/afp-2021-08-08/thys/? I think I needed to rename the folder so that it matches the exact description on the website. But I don't know why...
Robert Soeldner (Aug 13 2021 at 14:13):Yes, should be the case :)
Katharina Kreuzer (Aug 13 2021 at 14:28):Did you try isabelle components -u /home/rsoeldner/repo/afp-2021-08-08, ie without the /thys at the end?
Robert Soeldner (Aug 13 2021 at 14:35):yes, same error.
Katharina Kreuzer (Aug 13 2021 at 14:37):With and without the trailing /?
Robert Soeldner (Aug 13 2021 at 14:39):Yes
Katharina Kreuzer (Aug 13 2021 at 14:44):Oh, ok. isabelle components -u /home/kreuzer/afp worked for me, but if it doesn't for you, then I'm at the end of my wits.
Maybe have a look at https://isabelle.in.tum.de/dist/library/Doc/System/Misc.html, section Managing Isabelle components, if that can help you.
Anyone else has a suggestion?
Robert Soeldner (Aug 13 2021 at 14:45):Thank you Katharina
Mathias Fleury (Aug 13 2021 at 15:01):https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-May/msg00055.html is related to your issue
Last updated: Apr 23 2024 at 16:19 UTC