search

jsiek / deduce

A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.
59 stars 3 forks source link

Make deduce able to operate on multiple files #9

Closed Temperz87 closed 1 month ago

Temperz87 commented 1 month ago

Right now deduce cannot operate on multiple files, it can only deduce one file per command, but it'd be nice if it could. On the command-line-branch, I've started adding support for this, but I don't have the brainpower to figure out why the uniquify pass has side effects.

jsiek commented 1 month ago

What benefit do you see to deduce being able to operate on multiple files?

Temperz87 commented 1 month ago

I think that it'd help with organization and testing. Taking Nat.pf as an example, there are a ton of theorems in there, which could probably be put into many different files instead of just "Nat.pf" (e.g. "Nat-assoc-theorems" "Nat-commute-theorems" "Nat-implementation"), however if I wanted to test all of those files I would have to run "deduce Nat-assoc-theorems", "deduce Nat-commute-theorems", and "deduce Nat-implementation". While this problem can be "solved" by having all of the Nat theorems in one file, it runs goes back to the problem of one file doing a lot, and having to sift through a lot of hay in order to find a needle, which admittedly you could do with a Ctrl+f search. If deduce however could operate on multiple files with one command, you could say something along the lines of "Hey, do my Natural numbers work?" and point it towards the Nat directory. Another example can be seen in the Makefile, where right now it's running the deduce command a ton of times, which it'd be better to either feed in multiple files, or a directory.

Tl;dr: makes it easier to test multiple things at once.

jsiek commented 1 month ago

Update: now it handles multiple files. So the next step is to add support for processing a directory.