search

lecopivo / scientific-computing-lean

work in progress book on Scientific Computing in Lean
https://lecopivo.github.io/scientific-computing-lean/
10 stars 2 forks source link

suggest: manage code examples and text together #2

Closed Seasawher closed 1 week ago

Seasawher commented 7 months ago

Hi. Thank you for developing the excellent library. I look forward to the completion of the book.

I have seen the structure of the book, but with this structure, don't you have to manage the code examples and the text separately?

What about generating markdown files from Lean files with a tool and turning them into a book in mdbook? This is similar to the way adopted in the metaprogramming book.

lecopivo commented 7 months ago

Yes that is definitely the plan and I'm reusing Functional Programming in Lean. All the machinery for this is there. I just didn't set it up yet and up to only few days ago 90% of the code didn't compile as SciLean was missing features :) Because I'm building a very generic library I never had to create a 2x2 matrix which turned out to be a problem when writing examples in the book :)

lecopivo commented 7 months ago

Also I'm wondering what is the progress with Verso and if I should wait for it or adopt the existing mdbook workflow l

Seasawher commented 7 months ago

verso is still under development. mdbook is a good choice.

Seasawher commented 1 week ago

nice!