[isabelle-dev] Isabelle/VSCode bootstrap issue: "SML lexical error: bad input..."
kevin.kappelmann at tum.de
Wed Apr 20 13:45:27 CEST 2022
First I want to thank Makarius and the people involved at TUM for
brushing up Isabelle/VSCode! Secondly, I want to report an - I suppose
parsing - issue when bootstraping Pure. Steps to reproduce in
1. Start Isabelle/VSCode by using `isabelle vscode -l HOL`
2. Create and open a theory `Scratch.thy` with content
val _ = METHOD
3. Open `method.ML` (e.g. ctrl+click on `METHOD` in `Scratch.thy`)
4. Open `Pure/ROOT.ML` and wait for the bootstrap process
5. An error appears in the Isabelle output panel:
SML lexical error: bad input (line 229 of
On 25.03.22 13:38, Makarius wrote:
> *** Isabelle/VSCode Prover IDE ***
> * VSCodium, an open-source distribution of VSCode without MS
> telemetry, has been bundled with Isabelle as add-on component. The
> command-line tool "isabelle vscode" automatically configures it as
> Isabelle/VSCode and starts the application.
> * Command-line tools "isabelle electron" and "isabelle node" provide
> access to the underlying technologies of VSCodium, for use in other
> applications. This essentially provides a freely programmable Chromium
> browser engine that works uniformly on all platforms.
> This refers to Isabelle/73034d385688, which also provides an updated
> README.md: VSCodium shows that in the regular extension dialog.
> After some weeks of struggling with the underlying technologies, the
> required patches to VSCodium turned out rather simple, see
> This is the first time to make it semi-public. There are many small and
> big questions that are still open, see details in
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev