Strange "lake build" error msg

Stream: CSLib

[Ching-Tsun Chou]

I'm at this branch:
https://github.com/ctchou/cslib/tree/omega-flatten
When I do "lake build", I got the following error msg. But I can't find any occurrence of Mathlib.Computability.DFA in the whole repo. For that matter, I can't find any occurrence of noConfusionType, either. What is wrong?

✖ [7267/7268] Building Cslib
trace: .> LEAN_PATH=/Users/ctchou/play/cslib/.lake/packages/Cli/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/batteries/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/Qq/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/aesop/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/importGraph/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/plausible/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/packages/mathlib/.lake/build/lib/lean:/Users/ctchou/play/cslib/.lake/build/lib/lean /Users/ctchou/.elan/toolchains/leanprover--lean4---v4.24.0-rc1/bin/lean /Users/ctchou/play/cslib/Cslib.lean -o /Users/ctchou/play/cslib/.lake/build/lib/lean/Cslib.olean -i /Users/ctchou/play/cslib/.lake/build/lib/lean/Cslib.ilean -c /Users/ctchou/play/cslib/.lake/build/ir/Cslib.c --setup /Users/ctchou/play/cslib/.lake/build/ir/Cslib.setup.json --json
error: Cslib.lean:1:0: import Mathlib.Computability.DFA failed, environment already contains 'DFA.noConfusionType' from Cslib.Computability.Automata.DFA
error: Lean exited with code 1
Some required targets logged failures:

• Cslib
  error: build failed

[Kim Morrison]

The problem is that you define a type DFA, but Mathlib already does this.

[Kim Morrison]

See #CSLib > namespacing @ 💬 :-)

[Kim Morrison]

noConfusionType is a built-in helper type created anytime an inductive type is defined. It's not the clearest or most actionable error message, sadly.

[Ching-Tsun Chou]

I think the issue may be that when @Fabrizio Montesi added the DFA file to the main branch, he did not add their paths to Cslib.lean and hence the problem was not exposed at that point. While working on my branch (which is based on main), I did a lake exe mk_all which caused all the missing paths being added to Cslib.lean and the problem to show up.

[Ching-Tsun Chou]

@Fabrizio Montesi , does cslib require that all theory files have their paths be included in the top-level Cslib.lean?

[Fabrizio Montesi]

We don't have a requirement per se yet, but maybe we should? This should've been caught earlier, after all.

[Ching-Tsun Chou]

I think we should. Allowing some theory files to not appear in Cslib.lean introduces another level of complexity.

[Shreyas Srinivas]

If you don’t add those paths I don’t think lake even builds them by default, but even if it does (correct me if I am wrong), you want to make it possible to use a shorter prefix to import a whole folder for example

[Alexandre Rademaker]

I prefer explicit import, simpler and maintainable.

[Chris Henson]

In our lakefile, we have:

[[lean_lib]]
name = "Cslib"
globs = "Cslib.*"

which should build everything, right? I believe the intent was to not have the possibility of forgetting a file.

[Chris Henson]

Maybe this is not explicit, but I find it better for the "simpler and maintainable" aspect. If there are other tradeoffs, please let us know.

[Chris Henson]

There is also some automated review of imports (see cslib#83 for example) that I think covers this already?

[Chris Henson]

If that's true, we have a double assurance that everything is built and explicitly imported.

[Shreyas Srinivas]

Alexandre Rademaker said:

I prefer explicit import, simpler and maintainable.

You can achieve that with min_imports after developing a file. During development a large import is simpler.

I have never used this glob pattern in your lake file before, so maybe it works. Do check if you can cross import one file from another one in a different subfolder.

[Shreyas Srinivas]

About namespacing, I recall making some effort to get Mathlib Vectors namespaced last year, but this was not considered something necessary for the wider library. This namespacing (and it might bite even more with notation) is a constant headache. I suggest namespacing from the get go.

[Shreyas Srinivas]

Happy to make the PR to all files in an hour. It will touch many files so the sooner we do it the better. I'll start right away.

[Chris Henson]

Shreyas Srinivas said:

Happy to make the PR to all files in an hour. It will touch many files so the sooner we do it the better. I'll start right away.

This would be appreciated. I think the other thread reached consensus on Cslib as the top namespace.

[Shreyas Srinivas]

I think this name convention should be uniform. Anyway changing the namespace will be a matter of Ctrl + Shift +F > namespace CSLib

[Shreyas Srinivas]

You don't want any confusion between import name and namespace

[Shreyas Srinivas]

Whichever you pick

[Shreyas Srinivas]

(It seems the convention is already Cslib, so we can go with that)

[Shreyas Srinivas]

Here: https://github.com/leanprover/cslib/pull/105

[Shreyas Srinivas]

I just need to fix four tests

[Shreyas Srinivas]

All four of them are guard_msgs which are erroring on the different namespaces which honestly makes no sense to me

[Shreyas Srinivas]

A couple of issues:

1. There seems to be a strange mix of sections and namespaces in the Automaton folder. I am only standardising linebreaks here.
2. I am establishing a convention that the top namespace declaration is one line after the module docstring and that there is always a linebreak between namespace related lines. It appears that things have been haphazard so far.
3. I am using a different namespace CslibTests for the tests folder.

[Shreyas Srinivas]

I also think there ought to be scoped notation instead of notation. This saves a lot of headaches later. Happy to do a separate PR for that

[Shreyas Srinivas]

@Chris Henson and @Fabrizio Montesi : can I comment out the four guard messages for now?

[Chris Henson]

I think I know about those tests, let me check first

[Kim Morrison]

It's not just tests, the build is failing in

- Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
- Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
- Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic

[Shreyas Srinivas]

Will check

[Shreyas Srinivas]

Right. I missed a whole subfolder there

[Shreyas Srinivas]

Now it should build

[Chris Henson]

Shreyas Srinivas said:

All four of them are guard_msgs which are erroring on the different namespaces which honestly makes no sense to me

This is intentional, it is a test to ensure some metaprogramming is respecting namespaces. We can remove the non-namespaced test now. I can do this and push to the PR.

[Shreyas Srinivas]

okay

[Shreyas Srinivas]

Also, fixed the whole FSub and Stlc folder

[Shreyas Srinivas]

Need CI approval

[Shreyas Srinivas]

Now only the namespace tests fill fail hopefully

[Shreyas Srinivas]

More errors. Will fix. Isn't there a git commit hook for this before I push?

[Kim Morrison]

I typically run lake build? :-)

[Shreyas Srinivas]

lake build passes now

[Shreyas Srinivas]

If you have a push hook then this is automatic and the push fails if the build fails

[Shreyas Srinivas]

I'll probably need permission to run CI again.

[Shreyas Srinivas]

CI passes

[Shreyas Srinivas]

You might want to have subfolder specific namespaces too. A lot of notation is wildly reused in CS, so it would be beneficial to scope the notation to the subfolder namespaces. But that's for subsequent PRs

[Chris Henson]

Some of the notation (and grind annotations) are scoped this way, but yes more could do this.

[Shreyas Srinivas]

Also I suggest merging this PR asap since it touches every file and each PR pending in the queue will be affected by the resulting merge conflicts. The longer we wait, the more PRs are created and thus get affected. Conversely each merged PR gives merge conflicts for this one.

[Chris Henson]

Sure, I'll ping tomorrow if it's still pending.

[Shreyas Srinivas]

Needs one more CI run (permission). I localised a couple of mathlib namespace opens

[Fabrizio Montesi]

Merged!
Thank you all for discussing and fixing this, all while I was sleeping. :grinning_face_with_smiling_eyes:

[Ching-Tsun Chou]

I just noticed that Cslib/Languages/CombinatoryLogic/Evaluation.lean was added to the "main" branch as part of cslib#57 without being also added to Cslib.lean. I have made a PR (cslib#114) to fix it. CC: @Fabrizio Montesi

[Ching-Tsun Chou]

Perhaps we should have some automatic check to enforce this?

[Chris Henson]

I think there is an action that will flag this, it just never ran for that PR because it was opened over a month ago. If you see another case of this not caught, ping me and I'll address it.

[Fabrizio Montesi]

merged, thx :)