Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help with using AFP from Isabelle on Windows

Email Gateway (Aug 22 2022 at 18:02):

From: 王淑灵 <wangsl@ios.ac.cn>
Dear Isabelle users,

I want to use AFP theories in my formalization and have downloaded the AFP directory to /Isabelle2017. I am using Isabelle/HOL on windows. So I run Cygwin-Terminal under Isabelle2017 directory, and run the following command:

echo /afp/thys >> ROOTS

but it says “bash: ROOTS: Permission denied”

Any solution please? Thank you very much for your help.

Best,
Shuling

Best regards,
Shuling Wang
SKLCS, Institute of Software, Chinese Academy of Sciences

Last updated: Nov 21 2024 at 12:39 UTC