pictures & diagrams

Stream: lean4

[Dean Young]

Can lean 4 create .png and .jpg files, perhaps with various simple commands to make circles, lines, and geometric figures?

[Eric Wieser]

It can run arbitrary subprocesses and other programs exist which can do these things...

[Eric Wieser]

But probably this is an #xy and you probably want #lean4 > Announcing ProofWidgets4.

[Adam Topaz]

@Kyle Miller wrote a raytracer in lean4. I think it had some pictures involved…

[Kyle Miller]

ppm files are a very simple format. I think all you might learn from the code is how to write to a file using a version of Lean from last June.

[Tomas Skrivan]

I'm using widgets to create and display SVGs. There is a demo that draws couple of lines and circles. However there is no function to export it to a file.

[Dean Young]

I made this python document recently for string diagrams. It generates a .png. Check it out, it just works.

StringDiagramGenerator.py

What do you folk know about previous efforts like this one but for Lean?

[Dean Young]

rbraid.png
secondtriangle.png
test13.png

[Dean Young]

cover.png

[Dean Young]

The operations * and + are overridden and perform the horizontal and vertical composition operations. The examples contain all of the fundamental bricks.

[Dean Young]

Meanwhile, it would be nice to connect it to my categories in Lean. But partially I am interested in the facility with images on its own.