Choice of project through the url does not work properly

[jnarboux]

Hi,

We have a piece of code that works with Lean 4.14 but does not work with Lean 4.15 (it is not the problem):

#eval Lean.versionString
macro "foo bar" : term => do `( True)
def p  := foo bar
#print p

We created an URL to the code using the version 4.14 (project duper):
https://lean.math.hhu.de/#project=DuperDemo&codez=MQUwbghgNgBAMiCA7AdGEAnAzgSwPZIDKALhjkgOYBQAthAMYZ4wBEAZnswEYQYswAuGMUw0YAXgB8MACbMABgAoYAFQwBXEAEoqMkGxgAHGIPEwO3XlWCGySYkapA

We can do the same thing with lean live:
https://live.lean-lang.org/#project=mathlib-stable&codez=MQUwbghgNgBAMiCA7AdGEAnAzgSwPZIDKALhjkgOYBQAthAMYZ4wBEAZnswEYQYswAuGMUw0YAXgB8MACbMABgAoYAFQwBXEAEoqMkGxgAHGIPEwO3XlWCGySYkapA

The URL-based choice of Lean version does not work completely: we get some red underlines in the editor window as if we were working with version 4.15, but we obtain the right output in the right panel as if we are using version 4.14.

I suspect that the Lean version is chosen only after a first evaluation using the default version.

Regards,

Julien