AFP installation on Mac · Beginner Questions

I'm a Mac user of Isabelle and trying to install the latest AFP file into my computer. I've downloaded the file and put it under /Users
/myself/. However, it seems the command "isabelle components -u /Users/myself/afp/thys" doesn't work, as the Terminal says "isabelle: command not found".

Does anyone know how to solve this? I'm grateful for any help. Thanks in advance!

Mathias Fleury (Jun 20 2023 at 15:11):

I guess that you did no put isabelle into your path so you have to give the full path:

~/Isabelle2022-vsce/bin/isabelle components -u /Users/myself/afp/thys

Tobias Rothmann (Oct 25 2023 at 11:36):

Or you can just add Isabelle to your path:
For convenience here the command if you've put Isabelle in your Applications folder:

echo -n 'export PATH="/Applications/Isabelle2023.app/bin:$PATH"' >> ~/.zshrc

Angeliki Koutsoukou-Argyraki (Jan 25 2024 at 15:00):

Hi, I'm installing the AFP to another new machine (Mac) and it seems I'm missing something. The path to my AFP is smb://MYDATA/HOME/afp and I've put Isabelle2023 in my Applications folder. Any tips? Thanks in advance

Mathias Fleury (Jan 25 2024 at 15:26):

So instead of installing Isabelle locally, you installed on an external drive. What is the error message you are getting ?

Mathias Fleury (Jan 25 2024 at 15:27):

I would expect /Applications/Isabelle2023.app/bin/isabelle components -u smb://MYDATA/HOME/afp/thys to work but…

Angeliki Koutsoukou-Argyraki (Jan 25 2024 at 15:41):

Thank you, this gives the error: " Illegal character ":" in path element "smb:" " .But I'm not sure what path I should use instead (this is a machine that belongs to the University, configured to my account

Angeliki Koutsoukou-Argyraki (Jan 25 2024 at 15:43):

Angeliki Koutsoukou-Argyraki (Jan 25 2024 at 15:47):

e.g. when I try alternatively
/Applications/Isabelle2023.app/bin/isabelle components -u /MYDATA/HOME/afp/thys
I get:
*** Bad component directory: "/MYDATA/HOME/afp/thys"

Fabian Huch (Jan 25 2024 at 15:48):

Components need file paths, not URIs -- you'll need to mount your drive and then use the path of your mountpoint.

Angeliki Koutsoukou-Argyraki (Jan 25 2024 at 18:10):

/Applications/Isabelle2023.app/bin/isabelle components -u /Users/me/Downloads/afp/thys

Stream: Beginner Questions

Topic: AFP installation on Mac

Chris_Y (Jun 20 2023 at 15:03):