Email Gateway (Sep 13 2023 at 08:56): Email Gateway (Sep 13 2023 at 08:56):From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Isabelle users,
Yesterday, after the official announcement of its release was posted on this
chat, I downloaded Isabelle2023 and installed it on my Windows 10 PC. Then, I
opened in Isabelle2023 the files related to a new AFP submission on which I am
currently working, which resulted in the following couple of questions which I
would like to ask you. I am pretty confident that Isabelle documentation would
suffice to answer them, but maybe some of you would already have quick answers
to them.
In more detail:
The name of my session is not listed in the session selector box of the
Document panel, so that I cannot select it and generate documents for it from
the editor. This happens even if I place the folder containing the theory
files, the bib and tex files, and the ROOT file under the %ISABELLE_HOME%
folder and open all those files in the editor, although all the files are
correctly processed and the theory files are closed by the "end" keyword.
Why does this happen, and how can I solve this issue?
In correspondence with each @{cite xxx} antiquotation, the following
warnings are displayed:
"Legacy feature! Old antiquotation syntax, better use "isabelle update -u
cite""
"Unknown session context: cannot check Bibtex entry [entry identifier]"
This happens even in the conditions described above.
Again, why does this happen, and how can I solve this issue?
Thank you in advance for any possible feedback, much appreciated!
Best regards,
Pasquale Noce
Email Gateway (Sep 13 2023 at 12:13):From: Makarius <makarius@sketis.net>
On 13/09/2023 10:56, Pasquale Noce wrote:
- The name of my session is not listed in the session selector box of the
Document panel, so that I cannot select it and generate documents for it from
the editor. This happens even if I place the folder containing the theory
files, the bib and tex files, and the ROOT file under the %ISABELLE_HOME%
folder and open all those files in the editor, although all the files are
correctly processed and the theory files are closed by the "end" keyword.
Why does this happen, and how can I solve this issue?
First you need to have proper session ROOT setup, with all source files
declared properly.
Second you need to add its root directory to the Isabelle tool in question,
e.g. "isabelle build -d DIR" for batch-builds or "isabelle jedit -d DIR" for
interaction.
- In correspondence with each @{cite xxx} antiquotation, the following
warnings are displayed:
"Legacy feature! Old antiquotation syntax, better use "isabelle update -u
cite""
"Unknown session context: cannot check Bibtex entry [entry identifier]"
This happens even in the conditions described above.
Again, why does this happen, and how can I solve this issue?
The NEWS file has some notes on cite, which have now become more formal.
By having a proper session ROOT (with the bib files as 'document_files') and
includings the corresponding directory in "isabelle jedit -d ..." it should
work. (Maybe after sorting out further fine points.)
Makarius
Email Gateway (Sep 13 2023 at 21:26):From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Makarius,
Thanks to your suggestions, it has been easy to make interactive document
generation work fine on my session.
Thank you very much, best regards,
Pasquale
Last updated: Apr 28 2024 at 16:17 UTC