Email Gateway (Aug 23 2022 at 08:42): Email Gateway (Aug 23 2022 at 08:42):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi List,
Isabelle's LSP server does not start and complains that
$ISABELLE_TMP_PREFIX does not exist:
No such directory: "$ISABELLE_TMP_PREFIX"
The error(s) above occurred in session
"HOL_requirements(Pure)"positionline=3offset=22end_offset=25file=/home/mathias_fleury/Documents/isabelle/isabelle-release/src/HOL/ROOT
(line 3 of
"/home/mathias_fleury/Documents/isabelle/isabelle-release/src/HOL/ROOT")
The problem can be solved by creating the missing directory
(/tmp/isabelle-<user-name>). I did not notice in Isabelle-RC1 because I
first launched Isabelle2019, which created the directory.
I have bisected the error to the commit:
changeset: 70984:c92ae7b0f3f1
user: wenzelm
date: Sun Oct 13 16:26:31 2019 +0200
summary: clarified sessions/directories;
However, I do not understand why this commit caused the problem. It
probably only became visible with this commit.
Thanks,
Mathias
Email Gateway (Aug 23 2022 at 08:42):From: Makarius <makarius@sketis.net>
This should be more robust in
https://isabelle.sketis.net/repos/isabelle-release/rev/391ea80ff27c --- but it
is difficult to get into such a situation in practice and test it properly.
Makarius
Email Gateway (Aug 23 2022 at 08:42):From: Mathias Fleury <mathias.fleury12@gmail.com>
Your commit fixed the problem.
Thank you,
Mathias
Last updated: Nov 21 2024 at 12:39 UTC