From: Daniel Marshall <dmarshall2@sheffield.ac.uk>
Hello,
I feel like this might be more of a Linux issue than an Isabelle one, but
maybe someone can give me advice anyway.
Recently when I try and carry out document preparation with Isabelle I get
a permission-related error, as follows:
$ ~/Isabelle2018/bin/isabelle document -d generated/document -o pdf -n
document
/tmp/isabelle-daniel/bash_script2399141179650865402: line 1: ./build:
Permission denied
Failed to build document in "/home/daniel/isabelle/generated/document"
The same problem occurs if I run the command as root, and whether or not
this document command is run automatically as part of an "isabelle build"
command or manually by me.
I have previously built documents in this way and not had this issue. Does
anyone know what could be causing this to happen now?
Thanks for your help!
Daniel
From: Makarius <makarius@sketis.net>
I would say you merely need a "chmod +x" on your ./build script, without
the original document directory; an probably also clean the generated
directory before re-generating everything.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC