isabelle-prover / proving-contest-backends

"proving-contest"-backends for several theorem provers
MIT License
12 stars 5 forks source link

Coq backend #2

Closed Armael closed 5 years ago

Armael commented 5 years ago

Remaining:

Questions wrt the grader<->poller plumbing: how is partial success handled again? As far as I can tell, at the moment the poller script can only answer (yes/no) + some text message. If the text message gets parsed afterwards, what is the format exactly? Also, how does this interact with allow_sorry?

wimmers commented 5 years ago

Yes, so you are right. It simply is a text message. For Isabelle, it contains a JSON that gives a mapping from 'tasks' to 'points'. We should discuss and fix that format. The obvious thing would probably be to use a free-form JSON that is parsed in a proof-assistant specific way in the frontend. However, it is probably not a good idea to introduce too much proof-assistant specific code in the frontend.

Armael commented 5 years ago

Merging, I think this is more or less ready now :).