Bootstrapping issue?

Stream: lean4 dev

[David Thrane Christiansen]

I took a shot at adding support for LSP's position encoding negotiation today, to make it easier to write tools that interface with Lean. It was easy getting messages from the client to the server to work right, but the server's messages to the client require a bit more work.

In particular, Lean.DeclarationRange includes a cached LSP-encoded position to avoid heavy IO in order to recompute it. Rather than have an application-wide invariant that these cached values always match the LSP client's setting, I figured I'd just compute all three allowed encodings and see if that caused problems in benchmarks. Having modified DeclarationRange.mk and the various instances in the module (including ToExpr instances), I encountered a strange issue when trying to build, namely errors of the form:

Lean/Parser/Attr.lean:43:2: error: failed to emit registration code for builtin 'Lean.Parser.Attr.instance.declRange': application type mismatch
  Lean.DeclarationRange.mk { line := 43, column := 23 } 23
argument has type
  Nat
but function has type
  Lean.EncodedPosition → Lean.Position → Lean.EncodedPosition → Lean.DeclarationRange

Following the code, it looks like the update to the ToExpr instance should have been responsible for fixing this, and this makes me think that I'm running into a bootstrapping issue - after all, blobs of syntax seem like the kind of thing that would migrate across stages!

I tried to follow the instructions to work around bootstrapping issues in https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md, which pointed to an example PR that modified stdlib.make.in and a NIx config file. It seems that the settings infrastructure has changed since then - there's now two Nix configurations (one a flake) and the setting in question has disappeared from stdlib.make.in. I tried re-adding it and rebuilding without luck. Are there updated instructions somewhere?

[David Thrane Christiansen]

Wait - I realized that I put too much stock in the examples and not enough in the text, and I missed the last paragraph. Sorry about that - I'll check back in if I get stuck again.

[David Thrane Christiansen]

OK, I've tried those options, and still no luck. The same errors are happening, and my theory is still that the generated code is using the old ToExpr instances. But I'll continue looking around a bit more.

[Mario Carneiro]

My immediate suggestion would be to try setting parseQuotWithCurrentStage in stage0/src/stdlib_flags.h

[David Thrane Christiansen]

Yeah, I set both that and prefer_native without luck

[David Thrane Christiansen]

It could also be that there's just a quotation somewhere that's building things by hand that I need to fix, which is what I'm currently skimming for

[Mario Carneiro]

could you post your branch somewhere?

[Mario Carneiro]

I have some possible suggestions for places to fix but I'm not sure if you have already modified them

[David Thrane Christiansen]

https://github.com/david-christiansen/lean4/tree/lsp-ecodings

[David Thrane Christiansen]

Thank you! This is only my second nontrivial patch, so I really appreciate the help

[Mario Carneiro]

okay so my theory is that the stage0 code of mkElabAttribute, which calls the bad ToExpr DeclarationRange implementation, is being run by @[builtin_attr_parser] when compiling stage1

[Mario Carneiro]

In order to fix this, I think you have to first fix the mkElabAttribute implementation, then update-stage0, then update the DeclarationRange type

[Mario Carneiro]

this is awkward because you have to generate code for a DeclarationRange type that doesn't exist yet

[Mario Carneiro]

Actually, maybe a simpler option, since declaration ranges are not essential for compilation, is just to comment out the declaration ranges stuff entirely from mkElabAttribute, update the DeclarationRange type, update-stage0, then restore declaration ranges support to mkElabAttribute

[David Thrane Christiansen]

Thank you for the suggestion! I'll give it a go.

[David Thrane Christiansen]

The suggestion worked - thank you again!

[David Thrane Christiansen]

Is it important to preserve a series of commits that include updates to stage0, or is it OK to squash it together?

[Sebastian Ullrich]

Yes, we always preserve the update-stage0 commits as is

[David Thrane Christiansen]

Do we have an expectation that every commit in the history passes the tests and generally works?

[David Thrane Christiansen]

I'm basically trying to figure out the best way to fix up this icky history here

[Sebastian Ullrich]

It is a nice-to-have but we only ever test it for the head commit of the PR

[David Thrane Christiansen]

Do the stage0 updates need to be alone in their commits? Our can the commit include the changes that were included in the stage0 update?

[Mac Malone]

stage0 updates are set apart in a single chore: update stage0 commit in the history (in every case I have seen).

[David Thrane Christiansen]

All right, thanks! Sounds like I've got some quality time with Git in my near future :)