[isabelle-dev] Isabelle/VSCode bootstrap issue: "SML lexical error: bad input..."

Kevin Kappelmann kevin.kappelmann at tum.de
Wed Apr 20 13:45:27 CEST 2022

Hi all,

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
theory Scratch
   imports Main

   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 

Best wishes,


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 
> Isabelle/src/Tools/VSCode/patches/.
> This is the first time to make it semi-public. There are many small and 
> big questions that are still open, see details in 
> https://makarius.sketis.net/repos/isabelle_vscode_development/file/tip/TODO.md 
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list