search

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

Proof marshaling #100

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

experiment proof marshaling possible tool for #82

etiennecallies commented 3 years ago

Marshalling works like a charm 👍🏻 lcm23 proof is only 885 characters long! I'll deploy it on preprod as soon as we merge coqnotations.

However I think it's not a good idea to hash proof like that, since it will very likely break backward compatibility. For example, you save/share many proofs, and we deploy a new feature like Cut. Since Proof object would have changed (with Cut_proof) marshalling may shift and unmarshalling your previously saved proofs may not work.

I would try to Marshal json object, since it's more likely to be backward compatible.

olaure01 commented 3 years ago

However I think it's not a good idea to hash proof like that, since it will very likely break backward compatibility. For example, you save/share many proofs, and we deploy a new feature like Cut. Since Proof object would have changed (with Cut_proof) marshalling may shift and unmarshalling your previously saved proofs may not work.

You are probably right. My idea was indeed more in the short term:

etiennecallies commented 3 years ago

My idea was indeed more in the short term:

  • I start a huge proof, I stop in the middle, I want to save it and start again tomorrow
  • or I build a nice proof, I want to send it to my friend so that he can play with / modify it

I agree with that. It's a share-proof feature not a save-proof feature.

olaure01 commented 3 years ago

Fixes #82