lindy-labs / aegis

Verify Cairo contracts in Lean 4
GNU General Public License v3.0
8 stars 0 forks source link

tests: perform expected comparison over Aegis/Tests/Test.lean #17

Closed RaitoBezarius closed 8 months ago

RaitoBezarius commented 8 months ago

This adds a very basic way to perform expected comparisons (without an update script).

We test that the Test entrypoint returns the same stdout/stderr. I do some chores in the same PR.

Contributes in a very rudimentary way towards #9, from what I see, mathlib4 does not have an expected output verification but does have a silent verification mechanism for many tests/ elements, I don't know if we want to repeat this or fan out to many tests and verify their output all the time à la Lean 4.