Symbolic dynamics and the Curtis-Hedlund-Lyndon theorem

Stream: Is there code for X?

[mdnestor]

I proved Curtis-Hedlund-Lyndon theorem as well as some basic results in symbolic dynamics https://github.com/mdnestor/SymbolicDynamics

[Kim Morrison]

Are you planning on PR'ing any of it to Mathlib?

Also, I see there is at least one sorry left in the repo.

Also, you should add some CI (e.g. just what lake new provides out of the box now) so one can see right from the github page that it builds.

[mdnestor]

indeed, would like to PR eventually. The main result is proved without sorry's but I would still like to flesh out the api to be more comprehensive/useful.

Do you have a reference for CI?

[Kim Morrison]

Sorry, it's all a bit new. If you just run lake +v4.11.0-rc3 new just_for_CI outside your project, and then copy the entire .github directory from the just_for_CI directory into your project, hopefully things should just work out of the box.

[Kim Morrison]

(I'm actually not sure why you don't have this already --- I think with the version of lake you used to create your project in the first place it should have just been created automatically. Perhaps you deleted these files? If you remember, it would be nice to hear, so we can try and get the new user experience right!)

[Gareth Ma]

(base) ✔︎ ~ cd /tmp
(base) ✔︎ tmp mkdir asdf
(base) ✔︎ tmp cd asdf
(base) ✔︎ asdf lake init
(base) ✔︎ asdf (master) ✗ ls -la
drwxr-xr-x@   - grhkm 17 Sep 02:10 .git
.rw-r--r--@   7 grhkm 17 Sep 02:10 .gitignore
drwxr-xr-x@   - grhkm 17 Sep 02:10 Asdf
.rw-r--r--@ 142 grhkm 17 Sep 02:10 Asdf.lean
.rw-r--r--@ 218 grhkm 17 Sep 02:10 lakefile.lean
.rw-r--r--@   7 grhkm 17 Sep 02:10 lean-toolchain
.rw-r--r--@  68 grhkm 17 Sep 02:10 Main.lean
.rw-r--r--@   6 grhkm 17 Sep 02:10 README.md

[Gareth Ma]

Same for lake new asdf

[Gareth Ma]

(no github folder)

[Gareth Ma]

only with the +v4.11.0-rc3 does it create the .github folder

[mdnestor]

@Kim Morrison This worked, thanks. I didn't remove any files manually, the project was created via lake new {project-name} math

[Kim Morrison]

Hmm... this is going to be a problem if everyone is using old versions of lake to run lake new.

[Kim Morrison]

@Mac Malone, do we have a plan for this? Is this a lake issue? An elan issue?

[Kim Morrison]

Given that lake autoselects the version when you are in a project, when you are not in a project surely it should use the latest stable version.

[Mac Malone]

@Kim Morrison The beta elan feature of eager resolution should solve this (as a default of stable will always eagerly resolve to the newest stable Lean).