multiple files

Stream: mathlib4

[Reid Barton]

How do I work on two files added to mathlib A.lean and B.lean, where A uses sorry, and B imports A?
lake build errors on the sorry and doesn't build an olean file for A

[Reid Barton]

And when I have B open it tries to build A and fails.

[Alex J. Best]

Does replacing sorry with admit help?

[Reid Barton]

I replaced with an axiom :upside_down:

[Reid Barton]

I used it in term mode a lot.

[Reid Barton]

OMG error: unused variable `h` [linter.unusedVariables]

[Reid Barton]

Yeah no kidding, it will be used in the proof.

[Reid Barton]

Am I in uncharted territory?

[Jon Eugster]

If you remove that setting fron the lakefile, does that work or would that invalidate all the cache?

[Jon Eugster]

That is DwarningsAsErrors

[Reid Barton]

It started rebuilding everything

[Reid Barton]

The good news is when I put it back, it only rebuilt the 5 files it got to before I stopped it!

[Reid Barton]

Maybe it's better for now to work in a project with mathlib as a dependency?

[Adam Topaz]

This same issue came up for me yesterday. Is using axioms really the only way?

[Reid Barton]

Certainly we're going to need some way to work on multiple files at once without being stopped by linter nonsense

[Patrick Massot]

I think we need a way to enable this DwarningsAsErrors only in CI, not when editing files.

[Yaël Dillies]

Also surely the unused variables linter should just shut up whenever a declaration uses sorry, no?

[Reid Barton]

That also sounds extremely reasonable

[Sophie Morel]

Adam Topaz said:

This same issue came up for me yesterday. Is using axioms really the only way?

I had the same issue too. My solution was to fill in all the sorry's in the imported file, which is suboptimal in general.

[Adam Topaz]

Ah I see now. It's all because of these lines in the lakefile?

-- These settings only apply during `lake build`, but not in VSCode editor.
def moreLeanArgs := #[
  "-DwarningAsError=true"
] ++ moreServerArgs

Maybe we can arrange for the CI to just add that flag as part of the build, and remove this from mathlib4's lakefile?

[Adam Topaz]

There must be a way to pass this flag directly in the lake build command in the CI itself, no?

[Ruben Van de Velde]

As long as we can still reuse the cache from ci

[Mario Carneiro]

The much simpler way to shut up the unused variables linter is to (1) use _ before the variable or (2) turn off the unused variables linter in the file or section

[Adam Topaz]

But the sorries causing errors is a bigger problem. It essentially means you cannot work with multiple files at the same time.

[Mario Carneiro]

Yaël Dillies said:

Also surely the unused variables linter should just shut up whenever a declaration uses sorry, no?

I don't think this is a good idea, because it's easy to cause that old issue where def foo (x : Nat) : Nat := sorry creates a constant function and theorems are suddenly really easy to prove by rfl

[Mario Carneiro]

using an axiom is a decent workaround, I use that in test files too sometimes

[Mario Carneiro]

but it's definitely more dangerous since it would also pass CI

[Adam Topaz]

That (using axioms) doesn't scale. If I'm working on some file with deeply nested structures with various obvious proof obligations that I'm too lazy to fulfill right now, I don't want to have to introduce 37 axioms just to be able to use this file in a second file I'm working on.

[Mario Carneiro]

I think moving CI to use -DwarningsAsErrors makes sense

[Mario Carneiro]

that's usually what I do in other languages

[Mario Carneiro]

It's not 37 axioms, it's 1 axiom mySorry {A : Sort _} : A

[Mario Carneiro]

and then you use mySorry instead of sorry

[Adam Topaz]

oh I see okay.

[Adam Topaz]

yeah that's fine then :)

[Adam Topaz]

But then I have to remember to remove 37 mySorries at some point

[Mario Carneiro]

well you should remove mySorry itself before it hits the PR

[Adam Topaz]

Well, I guess just removing the axiom will give all the errors.

[Mario Carneiro]

IIRC the roadmap directory also had a mySorry in it

[Reid Barton]

Mario Carneiro said:

(2) turn off the unused variables linter in the file or section

How do I do this?

[Reid Barton]

Mario Carneiro said:

Yaël Dillies said:

Also surely the unused variables linter should just shut up whenever a declaration uses sorry, no?

I don't think this is a good idea, because it's easy to cause that old issue where def foo (x : Nat) : Nat := sorry creates a constant function and theorems are suddenly really easy to prove by rfl

Renaming x to _x will not help with that. And meanwhile it adds a bunch of busy work that also needs to be undone later when/if you fill in the sorry.

[Reid Barton]

What would be cool is if sorry could generate something like sorryAx x, for each unused variable x in scope (or maybe just every variable in scope?)

[Reid Barton]

Unfortunately just writing mySorry x doesn't work (Lean doesn't seem to want to infer the type of mySorry as a function)

[Mario Carneiro]

Reid Barton said:

Mario Carneiro said:

(2) turn off the unused variables linter in the file or section

How do I do this?

The reason linter warnings mention the linter name is because it's an option that you can set

[Mario Carneiro]

set_option linter.unusedVariables false

[Mario Carneiro]

Reid Barton said:

What would be cool is if sorry could generate something like sorryAx x, for each unused variable x in scope (or maybe just every variable in scope?)

It should be every variable in scope, except possibly the implDetail variables like the theorem name itself since this can cause a weird interaction with the termination checker

[Mario Carneiro]

this sounds like a proposal for a sorry! tactic

[Reid Barton]

Doesn't sorry already behave as some special elaborator?

[Mario Carneiro]

it has an elaborator, not sure how special it is

[Mario Carneiro]

it elaborates to sorryAx _ IIRC

[Reid Barton]

Fair enough

@[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
  let stxNew ← `(sorryAx _ false)
  withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?

[Mario Carneiro]

note that tactic sorry has a separate implementation, also in terms of sorryAx

macro "sorry" : tactic => `(tactic| exact @sorryAx _ false)

[Reid Barton]

I guess it could be ... exact sorry right?

[Reid Barton]

If possible, I'd prefer to avoid adding yet another thing that you have to know and remember about to opt in to the correct behavior rather than the wrong one

[Reid Barton]

I guess that when the type of the sorry is a Prop, there's no need to make a term that depends on all the variables

[Mario Carneiro]

Sure, make an issue ig

[Reid Barton]

Anyways, I think the more urgent question is how we can get -DwarningAsError=true used only by CI, while still having it produce usable oleans. I guess Lean needs to be told that this flag doesn't olean compatibility?

[Mario Carneiro]

I'm pretty sure something like lake build --lean-args="-DwarningAsError=true" works, I need to look up the syntax

[Mario Carneiro]

the olean compatibility problem is solved as long as the user lakefile.lean is byte for byte equal to the one used by CI

[Reid Barton]

Oh wild

[Reid Barton]

I assumed it would be based on the actual flags used

[Reid Barton]

It seems like adding irrelevant whitespace to the lakefile doesn't invalidate my oleans

[Mario Carneiro]

It invalidates the cache key

[Reid Barton]

Oh I see, I'm not using any cache.

[Mario Carneiro]

looking at the code now, lake lets you set -K options which are accessible via get_config? to the lakefile, so we could put some code in meta if get_config? CI = true then ... and set -KCI=true on the CI command line

[Reid Barton]

In general I would expect that running lake build with different -K flags would cause recompilation, especially if this involves invoking Lean with different options.

[Mario Carneiro]

the oleans don't have the lake invocation that produced them written in their binary, so I don't see why?

[Reid Barton]

The experiment I did was to just comment out the "-DwarningAsError=true" line, and then lake build started rebuilding stuff. So there is some mechanism here we need to evade or disable.

[Mario Carneiro]

if you produce oleans with different configuration then okay, but if it has no effect on the end product I don't think lake is doing any additional caching

[Mario Carneiro]

yeah, changing the lakefile directly won't work

[Reid Barton]

Do you mean that lake is the thing doing the recompilation checking, via its own invalidation mechanism, and not lean?

[Mario Carneiro]

yes, of course

[Mario Carneiro]

lean doesn't do any dependency tracking at all

[Mario Carneiro]

it doesn't have a --make mode anymore, it just compiles what you tell it to

[Reid Barton]

how quaint!

[Mario Carneiro]

the model seems to be based on rustc / cargo interactions, or gcc / make

[Mario Carneiro]

the compiler just takes a bazillion flags telling it what to read and what to write and the build tool does dependency management and recompiles things intelligently

[Reid Barton]

Where is this state stored then? In these .trace files?

[Mario Carneiro]

I was thinking it was in the oleans but that makes more sense

[Mario Carneiro]

yes the .trace file contains a hash of the stuff which would invalidate the artifact if changed

[Mario Carneiro]

although if you use --old it ignores the hashes and uses modification date tracking instead

[Reid Barton]

This seems promising but I'm not sure how to reconcile these statements

1. Removing "-DwarningAsError=true" from moreLeanArgs causes recompilation
2. Adding irrelevant whitespace to the file doesn't cause recompilation
3. Passing lake a -KCI=true command line option doesn't cause recompilation even if the effect is to add something to moreLeanArgs

[Reid Barton]

I tested 1 and 2 but not 3.

[Mario Carneiro]

I am not sure yet what the mechanism is for (2)

[Reid Barton]

I do like these .trace files that are just hashes printed in decimal

[Eric Wieser]

Isn't catching every variable in scope going to do totally the wrong thing for:

variables {X Y : Type*} -- used elsewhere

def foo (a : ℕ) : ℕ := new_sorry

which would make foo take three arguments not one?

[Reid Barton]

Anyone got a shorter one than... (16 bytes) ?

-rw-rw-r-- 1 rwbarton rwbarton 16 May 31 22:57 ./build/lib/Mathlib/Algebra/Module/Opposites.trace

[Mario Carneiro]

looks like the hash of a lean module is the combined hashes of its olean and ilean files. So if you make a modification that doesn't affect either one then it won't be invalidated

[Reid Barton]

Wait what about the source? Is this a different kind of hash? Or do you mean the "hash of an imported lean file"?

[Mario Carneiro]

no the source is not hashed, that was my point actually

[Mario Carneiro]

however the ilean is quite overfit to the source because of things like line/col positions

[Reid Barton]

Doesn't lake rebuild an olean file if I edit the source file?

[Reid Barton]

Or is this handled some other way (like by modification time)?

[Mario Carneiro]

modification time is used, sometimes...

[Mario Carneiro]

this code is really abstract, it's hard to tell why it does anything

[Reid Barton]

I am afraid if I look at it I will get flashbacks to Cabal.

[Mario Carneiro]

it's peak functional programming

[Reid Barton]

(Did you know Cabal supports non-GHC compilers? ...I think?)

[Reid Barton]

Maybe it is easier to just test on a new project

[Mario Carneiro]

did you know lake supports lakefiles that aren't called lakefile.lean? (The server definitely doesn't!)

[Floris van Doorn]

Mario Carneiro said:

I don't think this is a good idea, because it's easy to cause that old issue where def foo (x : Nat) : Nat := sorry creates a constant function and theorems are suddenly really easy to prove by rfl

Most of the time we're using sorry for theorems, and it would be nice if the linter didn't flag those.