Email Gateway (Jul 02 2025 at 18:02): Email Gateway (Jul 02 2025 at 18:02):From: Florian Haftmann <florian.haftmann@cit.tum.de>
I am still using the plain old lxcisa0.informatik.tu-muenchen.de for
certain tasks
Recently, a problem emerged:
$ isabelle build -b Pure
*** [SQLITE_BUSY] The database file is locked (database is locked)
I am using rev c8d92d4ced73 and a minimal ~/.isabelle/etc/settings:
init_components
"${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}"
"$ISABELLE_HOME/Admin/components/main"
What is going wrong here? Maybe NFS makes problems.
Thanks for any hint,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jul 17 2025 at 07:47):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Recently, a problem emerged:
$ isabelle build -b Pure
*** [SQLITE_BUSY] The database file is locked (database is locked)I am using rev c8d92d4ced73 and a minimal ~/.isabelle/etc/settings:
init_components "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/
contrib}" "$ISABELLE_HOME/Admin/components/main"What is going wrong here? Maybe NFS makes problems.
Redirecting ISABELLE_HEAPS to /tmp/… helps.
Seems to be an issue with NFS.
Indeed, sqlite has some reputation to pose problems with network file
systems, or certain configurations of them.
Since there is a work-around, it is maybe not worth pursuing further.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Aug 31 2025 at 20:21 UTC