Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP, AutoCorres2, write permission

view this post on Zulip Email Gateway (Jul 26 2025 at 18:14):

From: Alain Kägi <cl-isabelle-users@lists.cam.ac.uk>
Is it the expectation that each user install their own writable copy of the
Archive of Formal Proofs?

I have installed AFP in a system-owned directory (/opt) retaining the
original file ownerships and permissions. Bottom line, I don't have write
permission to the AFP directory. Unfortunately, with this setup, building
AutoCorres2 fails with permission denied (command: isabelle build -D <path-to-AFP>/AutoCorres2). The CTranslationSetup theory wants to write
$AFP/AutoCorres2/c-parser/StrictC.lex.sml (command mllex on line 536)
and $AFP/AutoCorres2/c-parser/StrictC.grm.sig &
$AFP/AutoCorres2/c-parser/StrictC.grm.sml (command mlyacc on line 537).

I can grant write permissions to these files, but that does not seem an
ideal solution.

I'm using Isabelle2025 and afp-2025-07-24.

Thanks for your attention,
Alain

view this post on Zulip Email Gateway (Jul 27 2025 at 22:48):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
Hi Alain,

you only need write permission in AutoCorres2 to build these the first time (it’s just lex/yacc). Once they exist, everything should be read only. So you could build once, adjust access rights, and then should be Ok for a site installation of this specific entry.

Most entries will be read-only, but the AFP in general does not place any restrictions on what entries might generate or write, so other entries might similar things. I’d recommend a per-user installation if you want to make sure you’re not hitting any such cases.

Cheers,
Gerwin

On 27 Jul 2025, at 04:14, Alain Kägi (via cl-isabelle-users Mailing List) [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

Is it the expectation that each user install their own writable copy of the Archive of Formal Proofs?

I have installed AFP in a system-owned directory (/opt) retaining the original file ownerships and permissions. Bottom line, I don't have write permission to the AFP directory. Unfortunately, with this setup, building AutoCorres2 fails with permission denied (command: isabelle build -D <path-to-AFP>/AutoCorres2). The CTranslationSetup theory wants to write $AFP/AutoCorres2/c-parser/StrictC.lex.sml (command mllex on line 536) and $AFP/AutoCorres2/c-parser/StrictC.grm.sig & $AFP/AutoCorres2/c-parser/StrictC.grm.sml (command mlyacc on line 537).

I can grant write permissions to these files, but that does not seem an ideal solution.

I'm using Isabelle2025 and afp-2025-07-24.

Thanks for your attention,
Alain

Confidential communication - This email and any files transmitted with it are confidential and are intended solely for the addressee. If you are not the intended recipient, please be advised that you have received this email in error and that any use, dissemination, forwarding, printing, or copying of this email and any file attachments is strictly prohibited. If you have received this email in error, please notify me immediately by return email and destroy this email.

Last updated: Aug 20 2025 at 20:23 UTC