search

REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs
https://reprosec.org/
Mozilla Public License 2.0
8 stars 0 forks source link

refactor: move source files in separate directories #3

Closed TWal closed 2 months ago

TWal commented 2 months ago

Fixes #1.

What do you think about it @fabian-hk ?

fabian-hk commented 2 months ago

Looks good! I would probably move the DY.Lib.Event.Typed.fst and DY.Lib.SplitPredicate.fst files into a folder called utility or helper. What do you think about that?

TWal commented 2 months ago

I agree that it's a bit weird to have both source files and subdirectories in src/lib! However I think I prefer this to a directory for "everything that was not big enough to have its own dedicated subdirectory" (e.g. it is explicit what we will find in the state subdirectory, that is everything related to state management, whereas utility or helper is less explicit).

Another possibility would be to put DY.Lib.Event.Typed.fst in an event subdirectory (it is everything related to events) and DY.Lib.SplitPredicate.fst in an helper subdirectory (it is all the generic helpers we have now). But directories with single files is also a bit weird.

fabian-hk commented 2 months ago

I was also thinking about putting the DY.Lib.Event.Typed.fst into an event folder. I like your last suggestion. In my opinion, having a single file in a directory is not optimal but better than having them directly in the lib folder.