The notation feature breaks exports and shareable links

lionelvaux commented 3 years ago

Salut,

I have just tested the new notation feature, which is great! But exporting and shareable links won't work: exporting or visiting the generated link fails with "Technical error, check browser console for more details." as soon as the proof contains the unfolding of a notation.

The only thing that shows up in the browser console is :

<!DOCTYPE html>
<!-- Page generated by OCaml with Ocsigen.
See http://ocsigen.org/ and http://caml.inria.fr/ for information -->
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Error 500</title></head><body><h1>Internal Server Error</h1><p>Error 500</p></body></html> proof.js:1072:13
error proof.js:1073:13
Internal Server Error

I have checked that this is triggered by unfolding:

here is a link to a proof in presence of a notation that is not unfolded: everything is ok
here is a link to a proof of the same sequent, unfolding the notation: opening this link fails, exporting from the page that generated this link fails too

olaure01 commented 3 years ago

Not sure this feature is completely ready for testing.

etiennecallies commented 3 years ago

Thanks @lionelvaux for testing this feature, but indeed all features are not already working with notations yet. Proof-sharing should work now (you have to re-share your proof), but export-as-coq, export-as-latex are still under development.

ComputerAidedLL / click-and-collect

The notation feature breaks exports and shareable links #121