import clash?

Stream: condensed mathematics

[Daniel Selsam]

I tried to build lean-liquid (with all.lean) but I am unable to import both prop_92.complete and laurent_measures.thm69 at the same time. I am using:

• Liquid: c28cead13bc241aa30ea136b50c3b789e906ee40
• Mathlib: 98665267ecf115bbbee37ec22e6a4d23b183114c
• Lean3: a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82

I get the error invalid object declaration, environment already has an object named 'limit'. Depending on the import orders, sometimes it complains invalid object declaration, environment already has an object named 'partial_sum_geom' as well. Am I doing something stupid? If not, is this related to a known issue?

[Johan Commelin]

I expect that some decls need to be namespaced.

[Johan Commelin]

@Filippo A. E. Nuccio is all of thm69 in a new namespace?

[Johan Commelin]

Or are there things ending up in _root_?

[Filippo A. E. Nuccio]

Let me check

[Filippo A. E. Nuccio]

Something was in _root_, but I have now put evertyhing in the namespace thm71; I am pushing.

[Filippo A. E. Nuccio]

Done

[Daniel Selsam]

@Johan Commelin @Filippo A. E. Nuccio Thanks, it works now. Might it be relatively easy to run mk_all in the CI?

[Johan Commelin]

I guess that shouldn't be hard. But I'm bad at CI. @Ben Toner if you have some time and energy, would you mind looking into :up: ?

[Ben Toner]

It’s green again. For future reference, I just went to https://github.com/leanprover-community/lean-liquid/actions/workflows/nolints.yml and clicked “Run workflow”. This is always safe for anyone to try, in that running this workflow will either have no effect or will make things better.

[Johan Commelin]

Thanks!