Thanks!

I added some small style changes, but it is otherwise great !

To git@git.sr.ht:~vigoux/busybeaver
   e366421f84a0..5cfe4e7ee946  master -> master

On Tue Sep 17, 2024 at 8:59 PM CEST, Marcelo Fornet wrote:
> From: Marcelo Fornet <mfornet94@gmail.com>
>
> - Define ZFunction structure object
> - Build z-function table
>
> fix: rename structure so lean doesn't complain
>
> feat(zf): [WIP] Write proofs for z-function
>
> fix: More proves on z-function
>
> feat: continue the proof
>

Use SVG to generate the diagram.

The new subcommand is:
```
explore <machine> <length> <outfile>
```

We could add another feature to "truncate" the diagram up to a certain
length.

Signed-off-by: Thomas Vigouroux <me@vigoux.eu>
---
 Busybeaver/SpaceTimeDiagram.lean | 214 +++++++++++++++++++++++++++++++
 Main.lean                        |  27 +++-
[message trimmed]

Pushed.

To git@git.sr.ht:~vigoux/busybeaver
   631f0e5a7632..75453acb92e4  master -> master

Awesome, this indeed fixed the problem.

Thanks !
-- 
vigoux

Hi there,

I have been getting reproducible 500 errors when viewing a certain patch.

Here is the patch: https://lists.sr.ht/~vigoux/busybeaver-devel/patches/54985

On the archives, it is possible to view the emails correctly though: https://lists.sr.ht/~vigoux/busybeaver-devel/%3C20240911115950.271590-1-me@vigoux.eu%3E

Regards.

-- 
vigoux

Signed-off-by: Thomas Vigouroux <me@vigoux.eu>
---
 Busybeaver/Parse.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Busybeaver/Parse.lean b/Busybeaver/Parse.lean
index 7e367f64fe4d..babd8a213a33 100644
--- a/Busybeaver/Parse.lean
+++ b/Busybeaver/Parse.lean
@@ -38,7 +38,7 @@ def pstmt: Parsec TStmt := attempt do
 def pStateCode: Parsec <| Array TStmt := many1 pstmt
 
 def sep1 (el: Parsec α) (sep: Parsec β): Parsec (Array α) :=
-  do manyCore (do let _ ← sep; el) #[← el]
[message trimmed]

Signed-off-by: Thomas Vigouroux <me@vigoux.eu>
---
 Busybeaver/Parse.lean | 109 +++++++++++++++++++++++++++++-------------
 Main.lean             |  16 +++----
 2 files changed, 85 insertions(+), 40 deletions(-)

diff --git a/Busybeaver/Parse.lean b/Busybeaver/Parse.lean
index 9493b6b65b7e..7e367f64fe4d 100644
--- a/Busybeaver/Parse.lean
+++ b/Busybeaver/Parse.lean
@@ -15,47 +15,92 @@ def pdir: Parsec Turing.Dir := attempt do
   | 'R' => return .right
   | _ => fail s!"Expected one of L/R"
 
[message trimmed]

Make parsing respect [standard TM format](https://wiki.bbchallenge.org/wiki/Turing_machine#Standard_text_format).

Note that when updating (which will come in a latter patch), this will need to be changed following a change in API for Parsec: https://github.com/leanprover/lean4/pull/5115

Thomas Vigouroux (2):
  feat(parse): better parsing of machines
  fix: avoid panic on invalid code

 Busybeaver/Parse.lean | 109 +++++++++++++++++++++++++++++-------------
 Main.lean             |  16 +++----
 2 files changed, 85 insertions(+), 40 deletions(-)

-- 
2.43.0

Infer machine symbol/state space during parsing. Now the parser strictly respects the standard machine format.

Simplify the `decide` command to use this fact, removing the need for `nlabs` and `nsyms` arguments.

Signed-off-by: Thomas Vigouroux <me@vigoux.eu>
---
 Busybeaver/Parse.lean | 109 +++++++++++++++++++++++++++++-------------
 Main.lean             |  16 +++----
 2 files changed, 85 insertions(+), 40 deletions(-)

diff --git a/Busybeaver/Parse.lean b/Busybeaver/Parse.lean
index 9493b6b65b7e..7e367f64fe4d 100644
--- a/Busybeaver/Parse.lean
+++ b/Busybeaver/Parse.lean
[message trimmed]