Mathlib Bump

Stream: Equational

[Pietro Monticone]

The update-dependencies workflow raised an issue (equational#733).

Opened equational#734 to fix it.

[Pietro Monticone]

The update-dependencies workflow raised an issue (equational#775).

All Generated files are involved. It should probably be fixed by some working with ATPs.

[Pietro Monticone]

To fix it you should:

• Run scripts/update_mathlib.sh
• Run lake build
• Debug

[Pietro Monticone]

(deleted)

[Pietro Monticone]

Unfortunately I can't do it because I have not worked with these Generated files so I am not familiar enough.

[Pietro Monticone]

I will try to fix everything tomorrow, but then the ATP people should adapt their scripts to the changes, run them again and open a new PR.

[Pietro Monticone]

Fixed. The PR will be ready in a few minutes.

[Pietro Monticone]

Opened equational#778

[Pietro Monticone]

lean4checker found a problem in equational_theories.Equations.LawsComplete here:

uncaught exception: (kernel) unknown declaration 'testLawsUpto4_computation._nativeDecide_1'

[Shreyas Srinivas]

Well, why is native decide showing up there in the first place?

[Shreyas Srinivas]

Proofs shouldn't use native decide

[Pietro Monticone]

The docstring says

/--
Here we do the actual computation. For now using `native_decide`, more serious
engineering is necessary if we insist on using `by decide` here.
-/

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/blob/4f4be0058ae5372bd8d738e93428b85ef6845d8e/equational_theories/Equations/LawsComplete.lean#L317

[Shreyas Srinivas]

CC: @Joachim Breitner

[Pietro Monticone]

But it worked before this bump, right?

[Shreyas Srinivas]

We use the lean-action script for lean4checker so it should be downloading a lean4checker with a matching tag

[Shreyas Srinivas]

That being said, using native_decide is always a red flag

[Vlad Tsyrklevich]

Ah, this is my fault for introducing the finite includes everywhere--sorry for the trouble. I'm not very familiar with Lean/Mathlib convention, does it make sense to include Mathlib.Data.Finite instead of Mathlib.Data.Finite.Prod everywhere to avoid future breakage? I suppose it impacts build times slightly, but avoids having to encounter this issue again.

[Shreyas Srinivas]

We download mathlib's cache, so build times should not be affected at all. I don't see how this causes the native_decide issue

[Shreyas Srinivas]

native_decide trusts the compiler (the one that produces executable bytecode) to be faithful in, for example translating Nats. This can create false proofs iirc.

[Vlad Tsyrklevich]

Yes, I think native_decide is separate

[Shreyas Srinivas]

Btw, I am waiting for Joachim to respond because he would know better why lean4checker is flagging native_decide now

[Shreyas Srinivas]

I came across a thread where @Mario Carneiro (CC) was discussing this with Joachim. @Mario: I can't pinpoint why this failure is showing up only now.

[Mario Carneiro]

I think lean4checker should be able to handle proofs by native_decide

[Mario Carneiro]

lean4lean definitely can't though

[Joachim Breitner]

Sorry, missing context here. so after a mathlib bump lean4checker (not lean4lean, right?) is unhappy with the files? Assuming everything was proper before this could be an issue with lean4checker, maybe an incompatibility with the latest lean (which may be lean's fault).

Ah, I see the workflow has both lean4checker and lean4lean. But the native_decide isn’t new… @Mario Carneiro , does lean4lean silently accept proofs by native_decide, or does that mean that the lean4lean CI check was ineffective?

I’ll have a closer look.

Ok, can be reproduced locally, after building lean4checker using

~/build/lean/equational_theories $ lake env lean4checker/.lake/build/bin/lean4checker equational_theories.Equations.LawsComplete
lean4checker found a problem in equational_theories.Equations.LawsComplete
uncaught exception: (kernel) unknown declaration 'testLawsUpto4_computation._nativeDecide_1'

but the definition is there (if I check with #print inside the file), so given that it worked before, and because lean4 didn’t change a lot, I suspect an issue with some of these changes:
https://github.com/leanprover/lean4checker/compare/v4.13.0-rc3..v4.13.0
OTOH, with the above command line, this should just do replayFromImports m in both cases. Curious.

[Joachim Breitner]

Ah! It also happens on main, if I pass the module name directly! So I conclude that the CI setup was broken before (i.e. not checking all the files the way we were expecting), and due to the above fixes to lean4checker the CI setup became more thorough.

@Mario Carneiro , are you sure that lean4checker can handle native_decide?

[Mario Carneiro]

should be, it's using the kernel function which has no special option for disabling native_decide

[Joachim Breitner]

Ah, of course the current CI setup with

~/.elan/bin/lake env lean4checker/.lake/build/bin/lean4checker equational_theories

only checked that single module (which doesn’t define anything new); only since lean4checker 4.13.0 this means “check every module with equational_theories as the prefix”

[Joachim Breitner]

Mario Carneiro said:

should be, it's using the kernel function which has no special option for disabling native_decide

And the whole machinery to run native code is available?

[Mario Carneiro]

aha, actually maybe not

[Mario Carneiro]

the interpreter might not have been set up correctly by the mechanism lean4checker uses

[Joachim Breitner]

(Although even then I’d expect a different error message; the declaration testLawsUpto4_computation._nativeDecide_1 is the argument to ofReduceBool)

[Mario Carneiro]

still, it's a weird error message in that case

[Mario Carneiro]

you would expect something like "IR check failed, missing definition _nativeDecide_1"

[Shreyas Srinivas]

There was a recent change about the way lean4checker works. But that's not what changed I believe. I copied the mathlib setup

[Joachim Breitner]

That is what has changed, see the diff I linked above.

[Joachim Breitner]

Ok, so TL;DR:

• The lean4checker CI setup was not doing what it should be doing, but happens to be doing it now.
• lean4checker (likely) doesn’t support native_decide, so one has to either drop the proofs, drop the check, or restructure the repo to be able to check the proofs that don't use native_decide.

[Shreyas Srinivas]

Previously lean4checker would check all files inside lake search path

[Mario Carneiro]

it would be good to confirm this first though

[Shreyas Srinivas]

Now it only checks the .build path

[Joachim Breitner]

Shreyas Srinivas said:

Previously lean4checker would check all files inside lake search path

That would be true if --fresh was passed (or no module name was passed), but that flag is not passed, the script says:

~/.elan/bin/lake env lean4checker/.lake/build/bin/lean4checker equational_theories

[Joachim Breitner]

Anyways, off to bed, hope this investigation was useful

[Shreyas Srinivas]

No wait. There were three different things:

1. With no module specified lean4checker would check everything.
2. With a module specified lean4checker would only check that module and its submodules.
3. With a module specified and --fresh, lean4checker would check all dependencies again

[Joachim Breitner]

That’s the new behavior. Before the bump, it was

2. With a module specified lean4checker would only check that module
   and the module equational_theories of course doesn’t contain anything interesting.

[Shreyas Srinivas]

I recall that the change is that

1. By default lean4checker only checks the top level module

[Joachim Breitner]

Look at a current run on main:
https://github.com/teorth/equational_theories/actions/runs/11643750505/job/32424852116
4s to check all proofs? Clearly this was never doing any real work.

[Joachim Breitner]

Did you look at the diff that I posted? Both the changes to the documentation and the code are rather clear.

[Joachim Breitner]

(looking at this log, 44s for lean4lean are also implausible.)

[Shreyas Srinivas]

I'll look at it. For now: The CI works correctly for lean4checker now, am I correct?

[Mario Carneiro]

Joachim Breitner said:

(looking at this log, 44s for lean4lean are also implausible.)

(we've known about that for a while but I haven't had time to look into the issue)

[Joachim Breitner]

Shreyas Srinivas said:

I'll look at it. For now: The CI works correctly for lean4checker now, am I correct?

Yes, I believe so: It checks every module it finds in the search path that has equational_theories as a prefix.

[Shreyas Srinivas]

So previously there was no way to only check the current project at all?

[Joachim Breitner]

Yes, using some combination of find to run it on each file individually.

[Shreyas Srinivas]

I thought lean4lean and lean4checker had the same interface

[Mario Carneiro]

(I'm currently working on updating lean4lean to include the changes; as usual no one pinged me regarding changes so I have to fix this stuff after the fact)

[Mario Carneiro]

lean4lean should now do the new lean4checker behavior as well

[Shreyas Srinivas]

Currently lean4lean is run in the following way:
The script clones the main branch of lean4lean and if the toolchains don't match, it fails silently

[Shreyas Srinivas]

If toolchains match and build succeeds it runs lean4lean on equational_theories

[Shreyas Srinivas]

The native_decide proof that is being flagged is in the LawsComplete file

[Shreyas Srinivas]

Fwiw, the lean4checker change that you are linking to landed 3 weeks ago. I requested it

[Shreyas Srinivas]

It should have been already running correctly

[Shreyas Srinivas]

https://github.com/leanprover/lean4checker/pull/26

[Mario Carneiro]

Here's a basic test for native decide:

$ cat Lean4CheckerTests/NativeDecide.lean
theorem obvious : true = true := by native_decide
$ lake build Lean4CheckerTests.NativeDecide
$ lake exe lean4checker Lean4CheckerTests.NativeDecide
lean4checker found a problem in Lean4CheckerTests.NativeDecide
uncaught exception: (kernel) unknown declaration 'obvious._nativeDecide_1'

[Mario Carneiro]

Here's what lean4checker is doing, broken down in this simple case:

import Lean
open Lean

run_cmd
  let env ← getEnv
  Elab.Command.elabCommand (← `(theorem $(mkIdent `obvious) : true = true := by native_decide))
  let env' ← getEnv
  let some (.defnInfo ci) := env'.find? `obvious._nativeDecide_1 | throwError ""
  let .ok env := env.addDecl {} (.defnDecl ci) | throwError ""
  assert! env.contains `obvious._nativeDecide_1
  let some (.thmInfo ci) := env'.find? `obvious | throwError ""
  let .error (.other hi) := env.addDecl {} (.thmDecl ci) | throwError ""
  println! hi -- unknown declaration 'obvious._nativeDecide_1'

[Mario Carneiro]

what is interesting here is that it does in fact have obvious._nativeDecide_1 in the environment, and also that it is using the .other kernel exception, which the kernel itself doesn't really use, which suggests this is an IR exception being filtered through the kernel

[Joachim Breitner]

Shreyas Srinivas said:

It should have been already running correctly

Then how else do you explain the changes with the bump? Note that the lean4checker ci script checks out the revision matching the toolchain

git checkout "$toolchain_version"

and we are on 4.13.0-rc3 on main and 4.13.0 on the equational#775, and the changes are included in between these two tags.

(Sorry for being grumpy, I’m sleepy and tired, but may I kindly ask you to be more generous with the benfit of doubt. Off to bed, now for good.)

[Shreyas Srinivas]

Ah right. The PR was merged but the tag wasn't updated

[Shreyas Srinivas]

In hindsight it makes sense that the tag wasn't updated

[Shreyas Srinivas]

The lean4checker script in this repo is a slightly modified version of the one from lean-action

[Shreyas Srinivas]

@Pietro Monticone : equational#778 will fail until equational#780 is completed and merged

[Mario Carneiro]

here's what you have to do to make native_decide work:

import Lean
open Lean

run_cmd
  let env ← getEnv
  Elab.Command.elabCommand (← `(theorem $(mkIdent `obvious) : true = true := by native_decide))
  let env' ← getEnv
  let some (.defnInfo ci) := env'.find? `obvious._nativeDecide_1 | throwError ""
  let .ok env := env.addDecl {} (.defnDecl ci) | throwError ""
  assert! env.contains `obvious._nativeDecide_1

  -- steps lean4checker doesn't do
  let some (.defnInfo ci) := env'.find? `obvious._nativeDecide_1._cstage1 | throwError ""
  let .ok env := env.addDecl {} (.defnDecl ci) | throwError ""
  let .some decl := IR.findEnvDecl env' `obvious._nativeDecide_1 | throwError ""
  let env := IR.declMapExt.addEntry (env.addExtraName decl.name) decl

  let some (.thmInfo ci) := env'.find? `obvious | throwError ""
  ofExceptKernelException (env.addDecl {} (.thmDecl ci))

[Mario Carneiro]

so in summary this is indeed an IR check error

[Joachim Breitner]

Great analysis! So probably a bug that's to be fixed in lean4's Replay module? (Maybe guarded by a flag - maybe some users of lean4checker don't want the checked file to run arbitrary code.)

[Mario Carneiro]

@Kim Morrison Why is Lean.Replay in lean instead of lean4checker now? It would be easier to fix this from lean4checker?

[Mario Carneiro]

(I don't think Lean.Replay can be used for anything except doing literally lean4checker as is.)

[Mario Carneiro]

even lean4lean can't reuse that function

[Shreyas Srinivas]

We should leave a summary of what happened for @Terence Tao 's notes:

Basically, my lean4checker PR had a mistake. It is three weeks now, so my memory is a bit hazy, but the cause must have been some combination of "I assumed I was already using the changes of lean4checker's update from 3 weeks ago" and "I assumed lean4checker worked on a similar interface as lean4lean". However the lean-action script was fetching a specific tag of lean4checker from before this update, namely v4.13.0-rc3 and thus not including lean4checker#26 .

The requested change landed in toolchain 4.13.0, and automatically lean4checker started running correctly with the repository's toolchain bump. It caught the use of native_decide in equational_theories.Equations.LawsComplete. @Joachim Breitner figured out that prior to the toolchain update lean4checker had been running incorrectly, and we discussed and figured out the rest.

@Mario believes that lean4checker ought to be able to handle native_decide and has a fix

[Shreyas Srinivas]

(apologies for my mistake btw)

[Mario Carneiro]

I don't have a fix

[Mario Carneiro]

I have concepts of a plan

[Mario Carneiro]

TBH I would really love to be able to evaluate native_decide in lean4lean. But this requires extracting a specification from the compiler, which is very hard

[Terence Tao]

This is primarily a long term issue though regarding whether we can generate a fully validated Lean proof of our impicatoin graph, right? In the short term we could just disable the leanchecker if needed, presumably.

[Mario Carneiro]

or just comment out that proof in lawscomplete

[Shreyas Srinivas]

equational#780

[Shreyas Srinivas]

But this PR uses the earlier toolchain so lean4checker is still not running correctly

[Joachim Breitner]

Terence Tao said:

This is primarily a long term issue though regarding whether we can generate a fully validated Lean proof of our impicatoin graph, right? In the short term we could just disable the leanchecker if needed, presumably.

It’s not even the implication graph, it’s just the theorem “all canonical size-4 equations are in our list”

[Joachim Breitner]

Shreyas Srinivas said:

But this PR uses the earlier toolchain so lean4checker is still not running correctly

Plus it doesn’t work :-). Ignore this PR for now, that’s why it's a draft

Oh, it actually passed the build step in 4mins. That’s someting … not really tenable yet, but it’s a start.

[Shreyas Srinivas]

Where did it fail? I see that lean4lean appears to be running correctly (it fetches master after all)

[Shreyas Srinivas]

But the check wasn't completed

[Shreyas Srinivas]

Mario Carneiro said:

or just comment out that proof in lawscomplete

I prefer this.

[Pietro Monticone]

Sorry, but it’s been a very busy day and I’ve not been able to interact on Zulip.

Tomorrow I can comment out the proof in LawsComplete in the Bump PR equational#778 if you all agree.

[Shreyas Srinivas]

@Mario Carneiro : Since the update lean4lean has been failing on all CI runs

[Mario Carneiro]

you should comment it out and make a PR turning it back on

[Mario Carneiro]

that CI step was never properly tested to begin with

[Shreyas Srinivas]

It's a bit late for me so i can't look into it now, but that's basically what I plan to do.

[Shreyas Srinivas]

I think the error might be in my script. lean4lean seems to be launching its own process.

[Shreyas Srinivas]

and my process quits separately

[Pietro Monticone]

Ok, so tomorrow I’ll comment it out, merge and then wait for the new PR by @Shreyas Srinivas.

[Shreyas Srinivas]

Merged the commented out version

[Shreyas Srinivas]

This one is for fixing the lean4lean checker: https://github.com/teorth/equational_theories/pull/782

[Shreyas Srinivas]

the script directly returns the return code of lean4lean directly. So if lean4lean fails, then the bug isn't in the script.

[Shreyas Srinivas]

The check appears to have succeeded

[Shreyas Srinivas]

On the other hand, I am not convinced with the verbose output. On a successful run I get 25k lines:
https://github.com/teorth/equational_theories/actions/runs/11647804605/job/32433484220?pr=782#step:13:25134

[Shreyas Srinivas]

However the "failed" run ended like this : https://github.com/teorth/equational_theories/actions/runs/11647168925/job/32432114332#step:13:49020
Nvm it seems fine now

[Notification Bot]

14 messages were moved from this topic to #Equational > LawsComplete by proof term generation by Joachim Breitner.

[Pietro Monticone]

I have merged main into equational#778 and now is ready to be merged.

[Shreyas Srinivas]

Let's hold on that

[Shreyas Srinivas]

Have we commented out the theorem using native decide for now?

[Shreyas Srinivas]

Also why have so many files changed?

[Shreyas Srinivas]

We know that Finite.Basic vs Finite.Prod wasn't the issue right?

[Pietro Monticone]

Mostly due to the deletion of the Mathlib.Data.Finite.Basic from the new Mathlib version

[Pietro Monticone]

Shreyas Srinivas said:

Have we commented out the theorem using native decide for now?

This issue has been solved by Mario’s PR I merged before updating the “fix-bump” branch.

[Shreyas Srinivas]

Is this equational#784?

[Shreyas Srinivas]

I thought that was still a WIP

[Shreyas Srinivas]

Well in that case I guess we should merge 778

[Pietro Monticone]

There is WIP on LawsComplete (see related thread), but it’s enough to merge the fixed bump. I’m going to merge it now.

[Shreyas Srinivas]

Okay :+1:

[Pietro Monticone]

Done :check:

[Shreyas Srinivas]

The good news is that both lean4checker and lean4lean appear to be working correctly now.

[Shreyas Srinivas]

The (not too) bad news is that CI times will go up substantially. Lean4lean takes 15 mins

[Shreyas Srinivas]

@Pietro Monticone The CI fails on an invalid header. I am surprised by this since it worked well on your PR and because this error is usually caused by mismatched toolchains, which doesn't appear to be the case

[Shreyas Srinivas]

I have re-run the CI for now

[Pietro Monticone]

It fails only when it retrieves from cache.

I have deleted the cache just to show that CI will succeed in this case (both in main and in the latest Mario's PR #788).

[Kim Morrison]

Mario Carneiro said:

(I'm currently working on updating lean4lean to include the changes; as usual no one pinged me regarding changes so I have to fix this stuff after the fact)

Sorry, didn't realise you were using the same CLI interface. Could you put a note somewhere in lean4checker (either README or probably better where the CLI interface is defined) reminding any future author of changes to either ping lean4lean or PR corresponding changes there?

[Pietro Monticone]

The update-dependencies workflow raised an issue (equational#790).

These are the files involved:

• equational_theories.DecideBang
• equational_theories.Equations.Command
• equational_theories.LiftingMagmaFamilies.

[Pietro Monticone]

Opened draft PR equational#793

[Pietro Monticone]

I have upgraded all the deprecated lemmas and solved the problem in equational_theories.LiftingMagmaFamilies.

Regarding equational_theories.DecideBang, here and here we get the following error:

invalid `do` notation, expected type is not a monad application
  Name → TacticM Expr
You can use the `do` notation in pure code by writing `Id.run do` instead of `do`, where `Id` is the identity monad.

Does anybody know how to solve them?

[Pietro Monticone]

Regarding equational_theories.Equations.Command, here we get

unknown identifier 'getDeclarationRange'

[Damiano Testa]

Maybe a missing ?? docs#Lean.Elab.getDeclarationRange?

[Pietro Monticone]

Yes, but then we get a type mismatch

[Shreyas Srinivas]

@loogle getDeclarationRange

[loogle]

:exclamation: unknown identifier 'getDeclarationRange'
Did you mean "getDeclarationRange"?

[Damiano Testa]

Try wrapping inside a (<- get...).getD default and see if it works?

[Pietro Monticone]

invalid field 'getD', the environment does not contain 'Lean.Syntax.getD'
  __do_lift✝
has type
  Syntax

[Shreyas Srinivas]

There has been some renaming of array and list functions

[Shreyas Srinivas]

Check the release notes of 4.14.0-rc1

[Shreyas Srinivas]

@loogle getD

[loogle]

:exclamation: unknown identifier 'getD'
Did you mean "getD", Array.getD, or something else?

[Damiano Testa]

I meant (← getDeclarationRange (← getRef)).getD default: is this what you tried?

[Damiano Testa]

Using getD on the whole call, not just the internal variable.

[Pietro Monticone]

Now

  let ranges := {
    range := (← getDeclarationRange? (← getRef)).getD default
    selectionRange := ← getDeclarationRange? eqStx }

returns:

type mismatch
  __do_lift✝
has type
  Option DeclarationRange : Type
but is expected to have type
  DeclarationRange : Type

[Damiano Testa]

Is it maybe referring to the next selectionRange line now, where a similar workaround may work?

[Pietro Monticone]

Yes, thanks.

[Joachim Breitner]

Pietro Monticone said:

I have upgraded all the deprecated lemmas and solved the problem in equational_theories.LiftingMagmaFamilies.

Regarding equational_theories.DecideBang, here and here we get the following error:

invalid `do` notation, expected type is not a monad application
  Name → TacticM Expr
You can use the `do` notation in pure code by writing `Id.run do` instead of `do`, where `Id` is the identity monad.

Does anybody know how to solve them?

closeMainGoalUsing passes an extra argument to it's argument now, which we can ignore. Add an _ to the fun (don't recall if it goes before or after expectedType).

Also, decide! has been upstreamed, and can be removed here. decideFin! has to remain.

[Pietro Monticone]

closeMainGoalUsing `decideFin fun expectedType _ => do [...]

Worked. Thank you @Joachim Breitner

[Pietro Monticone]

Ok, just fixed all the remaining errors.

Now it's awaiting for CI and then it'll be ready to be merged.

Thank you @Damiano Testa and @Joachim Breitner for your help.

[Pietro Monticone]

Oh no...

Running lean4checker
  lean4checker found a problem in equational_theories.Closure
  uncaught exception: failed to read file '././.lake/build/lib/equational_theories/Closure.olean', incompatible header

Maybe we should comment out the Lean4Checker and Lean4Lean steps for now @Shreyas Srinivas

[Shreyas Srinivas]

Has lean4checker been updated?

[Shreyas Srinivas]

It could be a simple toolchain mismatch issue

[Shreyas Srinivas]

Also lean4lean is independent

[Pietro Monticone]

In any case, I think that we can comment it out for the moment and re-enable it at the end.

[Shreyas Srinivas]

Also this error is definitely not occurring for the first time

[Shreyas Srinivas]

What was our fix last time?

[Pietro Monticone]

It was invalid header, not incompatible header

[Shreyas Srinivas]

I want to resist the urge to turn off external checkers every time we run into an issue with them

[Pietro Monticone]

The "fix" last time was to remove the saved cache and re-run all action jobs. Just done it again.

[Shreyas Srinivas]

I think we should clear the cache on each version bump

[Shreyas Srinivas]

Github caching doesn't "understand" lean's version issues

[Pietro Monticone]

Yes, and it should do it...

[Pietro Monticone]

Oh... it's because of the restore-key stuff.

[Pietro Monticone]

Let me fix it.

[Shreyas Srinivas]

Let's document this issue in the paper plan. It can be an example of the kind of strange issues one can run into on these projects

[Pietro Monticone]

Can you do it? I don't have time now.

[Shreyas Srinivas]

Sure. I'll do it in the next two days

[Shreyas Srinivas]

The concept of stale caches is not unknown, nor are github cache issues, but we are in a sense describing our experience

[Pietro Monticone]

Fixed.

[Pietro Monticone]

New error! This time in Generate home_page/dashboard.md:

2m 57s
Run pip install pillow
Defaulting to user installation because normal site-packages is not writeable
Collecting pillow
  Downloading pillow-11.0.0-cp310-cp310-manylinux_2_28_x86_64.whl (4.4 MB)
     ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 4.4/4.4 MB 42.2 MB/s eta 0:00:00
Installing collected packages: pillow
Successfully installed pillow-11.0.0
extracting histogram...
Traceback (most recent call last):
  File "/home/runner/work/equational_theories/equational_theories/scripts/generate_dashboard.py", line 43, in <module>
    hist_result = subprocess.run(
  File "/usr/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['/home/runner/.elan/bin/lake', 'exe', 'extract_implications', 'outcomes', 'equational_theories', '--hist']' returned non-zero exit status 1.

I don't have time to fix it directly at the moment.

[Shreyas Srinivas]

Sounds like the first place to check is the extract_implications lean tool. Probably a toolchain issue.

[Shreyas Srinivas]

I do have a question though. Do we really want to have his constant toolchain bumping? It seems we don't substantially benefit from a weekly toolchain bump

[Terence Tao]

Perhaps reduce it to monthly?

[Shreyas Srinivas]

Updating to stable toolchains and cleaning up the incompatibilities seems better. That's a once in a month thing

[Shreyas Srinivas]

Yes exactly. stable toolchains are released once a month.

[Shreyas Srinivas]

I don't buy into the mathlib philosophy that we need the latest and greatest toolchain when we don't substantially benefit from it and we have to deal with these breakages every week. EDIT: Unless the changes are essential bug fixes or offer new lemmas/tactics we can use.

[Shreyas Srinivas]

As I suspected, there is an error in the function argument of mapIdx which is now expecting an Nat parameter, and not a fin Parameter

[Shreyas Srinivas]

HashMap's mapIdx function's index parameter changed from Fin to Nat from 4.13.0 to 4.14.0-rc1

[Pietro Monticone]

I have just run:

lake exe extract_implications outcomes equational_theories --hist

It returns:

uncaught exception: failed to read file '././.lake/build/lib/equational_theories.olean', invalid header

[Shreyas Srinivas]

You need to build the project first

[Shreyas Srinivas]

Then you will get the error that in equational_theories/Closure.lean i.val isn't a thing anymore

[Shreyas Srinivas]

The solution is to simply use i

[Pietro Monticone]

But this is not supposed to throw any error, right?

def DenseNumbering.fromArray {α : Type} [BEq α] [Hashable α] (elts : Array α) : DenseNumbering α :=
  let index := Std.HashMap.ofList (elts.mapIdx (fun i x => (x, i.val))).toList
  ⟨elts, index⟩

[Shreyas Srinivas]

Change i.val to i

[Pietro Monticone]

But that will introduce an error in the last index.

[Shreyas Srinivas]

If you hover the mouse over elts.mapIdx you will see that it's type signature has changed

[Shreyas Srinivas]

It won't. I am guessing they changed it to use get_elem_tactic automatically

[Pietro Monticone]

Indeed:

application type mismatch
  { in_order := elts, index := index }
argument
  index
has type
  Std.HashMap α (Fin elts.size) : Type
but is expected to have type
  Std.HashMap α ℕ : Type

[Shreyas Srinivas]

Btw, I am quite sure that's the only difference. I didn't make a PR, but I got as far as running the script successfully

[Pietro Monticone]

Maybe consider pushing directly to equational#793

[Shreyas Srinivas]

Sure

[Pietro Monticone]

Please run run_before_push.sh before pushing to the fix-bump branch.

[Pietro Monticone]

(deleted)

[Pietro Monticone]

Shreyas Srinivas said:

Sure

Fixed.

[Shreyas Srinivas]

There is an even bigger issue

[Shreyas Srinivas]

The closure file is not imported in equational_theories.lean

[Shreyas Srinivas]

This is why it doesn't show up in the build

[Shreyas Srinivas]

Anyway. Some fixes landing in a few minutes

[Shreyas Srinivas]

@Mario Carneiro : Why is lean4checker so much faster than lean4lean?

[Mario Carneiro]

last time I benchmarked it it was about a 20-30% slowdown

[Shreyas Srinivas]

https://github.com/teorth/equational_theories/actions/runs/11693290732/job/32564528425

[Shreyas Srinivas]

lean4checker ~9 minutes and lean4lean ~15:30 minutes

[Mario Carneiro]

you did run it in verbose mode...

[Shreyas Srinivas]

oh yeah that's fair.

[Mario Carneiro]

You can also run it in --compare mode, in which case any time lean4lean is more than 2x slower to check a definition compared to lean4checker (and also more than 1 second to check) it will print it out

[Mario Carneiro]

(this makes it even slower though, since it has to run both checkers)

[Pietro Monticone]

Merged equational#793 bumping to v4.14.0-rc1

[Pietro Monticone]

Merged equational#798 bumping to v4.14.0-rc2

[Shreyas Srinivas]

Can we please not update to every rc release?

[Shreyas Srinivas]

Maybe we need to change the update frequency in the CI?

[Shreyas Srinivas]

We can point the mathlib dependency ref to the stable branch to ensure this

[Pietro Monticone]

Maybe we should keep the same update-dependencies schedule, but effectively update only when it fails and automatically opens an issue.

[Shreyas Srinivas]

What does it mean to effectively update? There wouldn't be any extra failures unless we update

[Pietro Monticone]

By "effectively update" I mean:

1. Noticing the "failure issue"
2. Bumping manually
3. Fixing what needs to be fixed manually
4. Pushing or opening the related PR

[Shreyas Srinivas]

I am proposing that we don't update at all and avoid the issues until the once a month stable release. The whole point is to not fix breakages every week

[Pietro Monticone]

I sincerely believe that the average bumping pain after a week is high enough to justify such a frequency.

The more we wait, the higher and potentially more intricate will be the necessary fixes.

[Shreyas Srinivas]

That's not necessarily true. It is easier to fix breakages that updates introduce in one go.

[Shreyas Srinivas]

Also rc changes sometimes introduce regressions and bugs that get fixed in stable releases

[Pietro Monticone]

It's not necessarily true, but very likely (in my humble experience).

[Shreyas Srinivas]

I would prefer updating to stable releases overall. I have found it less painful

[Pietro Monticone]

Ok ok, let me change the schedule then.

[Pietro Monticone]

What's the schedule of stable releases?

[Shreyas Srinivas]

Approximately once a month

[Shreyas Srinivas]

If we pin mathlib's dependency in lakefile.lean to stable then the updates automatically happen from stable toolchain to stable toolchain

[Shreyas Srinivas]

There was some talk of changing this but I don't think it materialised yet

[Pietro Monticone]

Opened PR equational#800.

It will run on the first day of each month.

[Shreyas Srinivas]

Let's also pin the dependency branch to stable

[Shreyas Srinivas]

This way we skip the RCs

[Pietro Monticone]

Do you mean like this?

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "stable"

[Shreyas Srinivas]

Yes

[Pietro Monticone]

Done. Feel free to merge.

[Shreyas Srinivas]

Do keep in mind that this will result in downgrade to 4.13.0

[Shreyas Srinivas]

But and that we will have to change i to i.val again in Closure.lean

[Pietro Monticone]

Maybe it's better to do this from 4.14.0 onward

[Shreyas Srinivas]

I'd prefer to go ahead with it now. We don't know how many RCs will be made before 4.14.0 lands and how many times we have to put out fires

[Pietro Monticone]

I'm going to merge equational#800 without the rev = "stable" for now and go to bed. I'll take a look at it tomorrow (later).

[Johan Commelin]

Pietro Monticone said:

Opened PR equational#800.

It will run on the first day of each month.

Maybe the 5th is a bit safer. The release might not happen on the 1st, eg if the month starts with a weekend...

[Mario Carneiro]

probably the 15th is best if you want to avoid edge effects

[Kim Morrison]

There's a big advantage to bumping downstream projects to both stable and release candidate tags of Mathlib, not just the stable tags!

If you go from e.g. v4.13.0 to v4.14.0 in one go, then you have to deal with both how Mathlib changed over a month, and how Lean changed over that month in one go.

If you go from v4.13.0 to v4.14.0-rc1 and then to v4.14.0, then in the first step you just see the changes to the Lean (and how Mathlib had to change to cope) --- because typically these tags are only a day or two apart in time --- and in the second step you just see how Mathlib evolved over a month with the language held fixed.

[Kim Morrison]

The decision as to which one is better for a given project depends on how tightly coupled with Mathlib / evolving language features it is. But in the highly coupled case, I recommend bumping via the release candidates for a more digestible experience. :-)

[Shreyas Srinivas]

Sure, but I think this project is not necessarily benefiting from keeping up with the latest and greatest mathlib RC release

[Shreyas Srinivas]

It is only piling up weekly maintenance issues. The cost-benefit ratio is definitely much greater than 1

[Shreyas Srinivas]

In other words, there is some coupling with Lean's core and a bit of batteries and a little bit of Mathlib, but not much

[Pietro Monticone]

Thanks for your comments and recommendations! A good compromise could be to set a frequency of 2 weeks or something.

[Shreyas Srinivas]

Amd pin to stable please

[Pietro Monticone]

Fine, I’ll do it later. Let me just stress once again that I don’t think it is a great choice :sweat_smile:

[Shreyas Srinivas]

I take responsibility for the once in a month patching

[Pietro Monticone]

Shreyas Srinivas said:

But and that we will have to change i to i.val again in Closure.lean

There would be much more to change than that. Unfortunately I have no time at the moment to revert everything.

[Shreyas Srinivas]

I'll do that in the evening then

[Pietro Monticone]

Changed the workflow so that it runs 15th day of each month.

[Pietro Monticone]

Shreyas Srinivas said:

I'll do that in the evening then

Thanks a lot.

[Kevin Buzzard]

You can run your project how you like, but as an independent observer it seems crazy to undo a bunch of changes for a pretty flimsy reason ("we need to move to stable now rather than next month and in particular we need to move backwards, despite having been on non-stable for the entireity of the project so far") when you know you'll have to redo them later.

[Shreyas Srinivas]

I know it sounds like that, but the cost is offset by the number of times we will have to deal with breakages this month. We have already had to deal with it twice and we are just on RC 1 of v4.14

[Shreyas Srinivas]

I know it sounds like that, but the cost is offset by the number of times we will have to deal with breakages this month. We have already had to deal with it twice and we are just on RC 1 of v4.14

[Shreyas Srinivas]

This way, I am almost certain that the next time I deal with this issue will be on Dec 15

[Kevin Buzzard]

I'm just observing that explicitly going backwards sounds nuts. Why not just stay on whatever you're on right now and then go forwards to the next stable?

[Shreyas Srinivas]

Because staying on it means going through each RC release

[Kevin Buzzard]

What I'm implicitly worried about is that on Dec 15th you'll discover how much work is involved trying to move forwards by a long way all in one go, and give up, thus putting the project in a worse state. Have you seen how much work it is keeping mathlib up to date? I know this project is smaller but I'm concerned that you're just saying "I will take this job on" without really understanding what it entails.

[Shreyas Srinivas]

Although one workaround is to turn off auto update until 15 and pin to stable on a closer date

[Kevin Buzzard]

Shreyas Srinivas said:

Because staying on it means going through each RC release

I'm suggesting that the next bump you do is not to rc37 but forwards to the next stable. I'm not suggesting you keep up with all the rcs. This way you'll have to do less work, but even this smaller amount of work might be a surprisingly large amount of work.

[Shreyas Srinivas]

I think the trade off is we are fixing breakages once or twice a week at times and at a schedule dictated by RC releases

[Shreyas Srinivas]

Okay that's a fair point. Let's stay on rc1

[Pietro Monticone]

We’re are on RC2 already btw.

[Shreyas Srinivas]

And turn off the update script. Then we pin to stable on Dec 14th

[Kevin Buzzard]

This sounds like a much better idea!

[Shreyas Srinivas]

Pietro Monticone said:

We’re are on RC2 already btw.

Ah so three fixes in the last week alone

[Shreyas Srinivas]

Although rc2 was less effort

[Pietro Monticone]

No, for RC2 no fixes were required. That’s the point.

[Pietro Monticone]

I prefer to have much more control over small, temporally distributed fixes…

[Shreyas Srinivas]

That's good. But last week's update issues hit us back to back

[Shreyas Srinivas]

I want to avoid that and prefer a more predictable breakage schedule

[Pietro Monticone]

Not really, just a few import issues, a few deprecated lemmas, a few signature changes.

[Shreyas Srinivas]

For this project, we won't be suffering like Mathlib. Mostly our issues will be tactic changes, stuff moving to core, and api changes

[Shreyas Srinivas]

So the total work we do for updates will be more or less the same.

[Shreyas Srinivas]

I am just bunching up the changes to a more predictable schedule

[Shreyas Srinivas]

Ofc this means that once a month, I spend half a day making fixes

[Pietro Monticone]

I don’t know how anyone can confidently predict that, honestly.

[Shreyas Srinivas]

One can't. One can look at past experience and extrapolate

[Pietro Monticone]

If I do that, I arrive at the opposite conclusion :sweat_smile:. I think I’m not completely miscalibrated having managed all the updates in the project so far…

[Pietro Monticone]

I really tend to prefer avoiding the surprises we could get after a month.

[Pietro Monticone]

Maybe we can vote on this

[Shreyas Srinivas]

I'll leave it to you then. But in my experience, working simultaneously on 4 projects, I was spending an awful lot of time fixing update breakages than actually adding content. Since I started keeping them on stable, things have gotten much better

[Shreyas Srinivas]

And what's worse is there is no pattern to the release time of these RCs. They strike like lightning :high_voltage:

[Shreyas Srinivas]

This is fine for the purpose they serve, but not ideal for working efficiently on projects and keeping them reasonably up to date

[Pietro Monticone]

Since we’re going to upstream more things to Mathlib soon, we will need to bump it in order to use it and remove the local version.

Moreover, while proving we want to LeanSearch the latest version of Mathlib in order to avoid duplicates, etc.

[Shreyas Srinivas]

How frequently is LeanSearch's model retrained?

[Shreyas Srinivas]

Presumably not once a week?

[Shreyas Srinivas]

If that's the case then what is gained w.r.t leansearch by updating more frequently?

[Pietro Monticone]

I mentioned LeanSearch, but of course the same would be the case for Docs, Loogle, etc.

We don’t want to duplicate work and if a useful lemma has been added to Mathlib, we want to be able to use it.

When we upstream something to Mathlib we want to be able to import it and remove the local version quickly.

[Pietro Monticone]

I think the benefits of high-frequency (< 1 week) updates outweigh the costs

[Shreyas Srinivas]

Imho upstreaming should happen when a project is near completion and mostly stable

[Shreyas Srinivas]

At least in CS venues, the code contributions are usually part of the artefact, so it you upstream and import them, they dont get evaluated

[Pietro Monticone]

If the declarations we want to upstream are sufficiently self-contained, there is no reason to wait.

It happens very often with small lemmas which are missing in Mathlib.

[Shreyas Srinivas]

This is ofc subject to some level of interpretation across venues

[Shreyas Srinivas]

About what the core contribution is

[Pietro Monticone]

When we upstream we keep track of the project origin.

[Shreyas Srinivas]

Sure, but the upstreamed code isn't part of the artefact submission

[Pietro Monticone]

Should we care about that in our case?

[Shreyas Srinivas]

Again, this is beside the point. It you are happy to deal with RC breakages, I am fine. Last week we were fixing problems on two days past midnight

[Shreyas Srinivas]

Shreyas Srinivas said:

Sure, but the upstreamed code isn't part of the artefact submission

Imho yes. It's about ensuring correct academic attribution of the code.

[Pietro Monticone]

Ok, I would keep it high-frequency for this month. Let’s see…

[Mario Carneiro]

Shreyas Srinivas said:

And what's worse is there is no pattern to the release time of these RCs. They strike like lightning :high_voltage:

Keep in mind that RC releases (past rc1) are usually because we discovered some really important regression and patched it, so it might be a good idea to upgrade as soon as possible depending on what the bug is. (e.g. that one time when lake would delete your project...)

[Joachim Breitner]

Mario Carneiro said:

(e.g. that one time when lake would delete your project...)

Will this enter the mythodology of the lean community, similar to that old GHC bug where it would delete source files it found type-incorrect?

[Mario Carneiro]

wait that was a bug and not an easter egg?

[Joachim Breitner]

That was from way before my time, but the hearsay that I got always referred to it as a bug

[Shreyas Srinivas]

This I know. But these are usually buggy features for the next release. that is why I said they serve their purpose well. But it is also why migrating through RCs is not super useful always

[Shreyas Srinivas]

While migrating between stable versions may not necessarily be the easiest thing, I think the combined expected effort of working through the corresponding RC releases would be higher than just one bump to stabke

[Shreyas Srinivas]

After all it isn't like fresh new features are being introduced in each RC of a release as a matter of principle (might be different in practice)

[Shreyas Srinivas]

In fact that 4.1 RC bug is one reason I initially started avoiding them as much as possible

[Kim Morrison]

Shreyas Srinivas said:

Imho upstreaming should happen when a project is near completion and mostly stable

This is a recipe for disaster. Please please do not do this.

[Shreyas Srinivas]

Why? Isn't this usual? The bits and pieces that get upstreamed will have to be adapted for mathlib, which is extra work. Instead by putting off upstreaming we can save work and continue to use convenient definitions and theorems

[Shreyas Srinivas]

In fact, iirc, the project on godel's first incompleteness theorem as well as the one on flow matrices was already done before they started upstreaming PRs.

[Rémy Degenne]

From experience the issue is mainly that if you put off upstreaming until the end of the project, it will never actually happen. When the project ends, the interest of the participants decreases a lot, and moving things to Mathlib is not nearly as fun as doing new, other things. Also you'll have accrued a lot of stuff that will need constant adaptations during the move, and upstreaming will be a huge task.
Combine a huge task and participants that are not very interested anymore, and you get a project that forever stays in its own repository.

[Shreyas Srinivas]

Fwiw the upstreaming PRs are already being worked on. In this case we went ahead with our own definition of free magmas so every upstreaming PR is already starting on a big disadvantage.

Further I am thinking about this from the project's perspective. I know that CPP and ITP follow single blind reviewing so pointing to upstream content in your papers is not a big deal, but in strongly double blinded venues pointing to publicly hosted code with commit history and authorship headers will be a problem

[Kim Morrison]

I'm sorry, Shreyas, I'm not interested in arguing with you on this one, I'm just going to leave my advice as above.

[Mario Carneiro]

I'm interested to know what you mean by "recipe for disaster" though; did you mean worse consequences than what Rémy Degenne outlined?

[Mario Carneiro]

I wouldn't exactly classify that as a disaster, if you are not particularly motivated to get things in mathlib in the first place

[Kim Morrison]

Sorry, nothing more than what Remy says.

[Shreyas Srinivas]

I brought up that freemagma point because freely importing Mathlib is already not an option. No one has taken up the namespacing task I posted one or two weeks ago. So the project cannot necessarily easily import something that is upstreamed. The coupling with Mathlib is looser with this project than usual. Of course this shouldn't stop interested contributors from upstreaming stuff but most of that stuff is not likely to feed back into the project (ignoring the anonymity concerns above for the sake of discussion)

[Shreyas Srinivas]

So there is bound to be some divergence between what mathlib eventually gets and what the project uses anyway. And then there is the time the PR will spend on the queue. This alone will mean that the people making upstreaming PRs will have to stay motivated for a while and make changes as lean and mathlib get updates and as reviews come in.

[Alex Meiburg]

(Since this is the closest thing to a "lean4checker thread") in equational#829 I wanted to use native_decide, not because it was faster than decide (decide would be fast enough) but because there's a bad decidability instance Multiset.decidableForallMultiset. Of course ultimately it would be good to fix all the bad decidability instances in Mathlib ( :upside_down: ) but in the meantime, lean4checker means that it won't build. Is there anyway around this in the medium term?

[Shreyas Srinivas]

the conclusion above was that lean4checker and lean4lean both need substantial modification to allow native_decide

[Alex Meiburg]

Is there some attribute I can put on the relevant theorem, all_Magma_Fin2, to tell lean4checker to skip it? Like could I marking unsafe to get it skipped? Nothing else is depending on it.

[Alex Meiburg]

(That was a hypothetical - I know that there's no such thing as unsafe theorem - but I'm asking for something analogous)

[Shreyas Srinivas]

I don't know for certain, but I am going to make a guess that there isn't because the whole purpose of lean4checker is to disallow false environment manipulations.

[Shreyas Srinivas]

And removing a theorem from being checked appears to be basically just that. It is another matter that there is no downstream uses of it.

[Eric Wieser]

Alex Meiburg said:

Is there some attribute I can put on the relevant theorem, all_Magma_Fin2, to tell lean4checker to skip it? Like could I marking unsafe to get it skipped? Nothing else is depending on it.

axiom

[Shreyas Srinivas]

Doesn't the blueprint CI include a check for axioms?

[Eric Wieser]

Perhaps, but you could whitelist them one at a time

[Eric Wieser]

axiom two_plus_two : 2 + 2 = 4
example : type_of% two_plus_two := by native_decide

seems like a safe enough way to handle it

[Eric Wieser]

Which I assume succeeds in hiding native_decide from lean_checker

[Eric Wieser]

Alex Meiburg said:

but because there's a bad decidability instance Multiset.decidableForallMultiset

Is there a thread or issue about this?

[Shreyas Srinivas]

If this is not a hurry, and Mathlib will ship a new instance in a reasonable time frame, I would prefer to wait for it

[Shreyas Srinivas]

Also the linkifier is just equational#761

[Alex Meiburg]

Changing it from theorem to unsafe def makes lean check the correctness of the proof and lean4checker OKs it, so that's what I'll do for now. But I guess that leaves the separate question if it's okay to merge like that? Thoughts?

[Shreyas Srinivas]

I'd rather wait. In this particular instance it is fine insofar as no downstream theorem is using it. But this is about setting a precedent that can become unmanageable at scale.

[Shreyas Srinivas]

But yeah do ping as soon as the mathlib change is ready and available and you can circumvent native_decide

[Alex Meiburg]

Your point about waiting because it would be unmanageable at scale makes sense -- but I see that @Terence Tao just merged it actually, heh - maybe I should have marked as draft. Well, maybe we'll leave it merged, but yes it makes sense to avoid this as a pattern en large.

[Alex Meiburg]

I mean I'll defer to the maintainers

[Shreyas Srinivas]

I do think a build should flag unsafe defs that are Props, to manage the scale issue

[Terence Tao]

I think it's fine to have some less important side results that are explicitly marked as not subject to leanchecker so long as there is some way to still collect and flag them for future resolution. Though I agree that we don't want to start making a flood of such exemptions.

[Shreyas Srinivas]

Unfortunately I don't think there is any well known way to have lean flag this one later

[Shreyas Srinivas]

That's why I am hesitant about this PR

[Terence Tao]

We could open a low-priority issue to resolve it?

[Shreyas Srinivas]

I am not confident that we will remember to address it when the necessary mathlib changes arrive. Maybe we could use the roadmap feature of the project dashboard to remind us about this

[Alex Meiburg]

Is there some command like #lint "This should be a theorem" to just issue a lint warning 'manually' at build time?

[Shreyas Srinivas]

https://github.com/marketplace/actions/issue-duedate-reminder

[Shreyas Srinivas]

We could use that action to remind us to check this low priority issue

[Terence Tao]

OK. So we open an issue and also set some reminder to bring it up again on the Zulip after some fixed time or something?

[Alex Meiburg]

As one other option: if we set the proof to be first | decide | native_decide, then it will switch to using "decide" whenever that compiles. There might be a linter option to detect unsafe defs that don't need to be unsafe, which would then fire

[Shreyas Srinivas]

Terence Tao said:

OK. So we open an issue and also set some reminder to bring it up again on the Zulip after some fixed time or something?

Sounds like a viable idea

[Terence Tao]

Opened equational#834 for this.

[Mario Carneiro]

Alex Meiburg said:

but because there's a bad decidability instance Multiset.decidableForallMultiset

You can fix this yourself you know, just make an instance which overrides the original

[Mario Carneiro]

my inclination would be to put in workarounds to get it to compute with decide and avoid the mess that native_decide implicates

[Mario Carneiro]

and then pursue a mathlib PR to remove the workarounds

[Shreyas Srinivas]

@Alex Meiburg : Could you make a PR like this please

[Alex Meiburg]

Good point Mario, this genuinely hadn't occurred to me as a possibility :man_facepalming: Will do!

[Alex Meiburg]

Okay, I've been staring at this for an hour and I don't see any way to do it. (Since this isn't specific to Equational in any way, I'll start a thread in a different channel and then link here)

Link: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20bad.20Decidable.20instances.20for.20quotient.20types/near/482430599

[Alex Meiburg]

Alright, I'm embarrassed, turns out the issue was actually with my own instance, not mathlib's, so it was an easy fix. Should be fixed with equational#836. I guess I am not as capable of understanding decide's error logs as I thought I was.

[Pietro Monticone]

The update-dependencies workflow raised an issue (equational#840).

Opened equational#847 to fix it.

[Shreyas Srinivas]

Upstream import changes?

[Vlad Tsyrklevich]

I was debugging what turned out to be a trivial import issue from this mathlib bump, though it took me a while to figure it out. What is the usual way of debugging an issue like this? I thought about just using an 'import Mathlib' to see if I'm missing some obvious import (or if it's a deeper issue), but our instance of FreeMagmas conflict so that approach didn't work.

[Shreyas Srinivas]

Usually search the "unknown id" on the loogle extension or mathlib docs

[Vlad Tsyrklevich]

So in this case the specific error was that I was failing to synthesize a [Finite G->G] when I had a [Finite G], and that seems hard to search for? Is there a trick there?

[Shreyas Srinivas]

I think there is a #synth or #synthInstance command

[Shreyas Srinivas]

And then import Mathlib when you do it

[Shreyas Srinivas]

Even if you get other errors, you will get the instance you are looking for and you can ctrl Click and find it

[Shreyas Srinivas]

I haven't used this command ever, so I would recommend looking around on this zulip for examples of correct usage

[Vlad Tsyrklevich]

Thanks, I got that to work with some prodding and found the instance I think I needed though I'm still confused by what it actually does.