Timeline for What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 12, 2015 at 14:18 | comment | added | darij grinberg | "We're now trying to write an updated and more comprehensive document." That's wonderful news, thank you! | |
| Jul 12, 2015 at 14:07 | comment | added | Assia Mahboubi | You're right, the 2010 tutorial is outdated (at least for the Coq scripts), sorry about that. We're now trying to write an updated and more comprehensive document. But it will probably take an other few months to reach a readable state. Thus we should probably also try to maintain the old version alive meanwhile... | |
| Jul 12, 2015 at 13:42 | history | edited | Assia Mahboubi | CC BY-SA 3.0 |
grammatical error
|
| Jul 12, 2015 at 10:13 | comment | added | darij grinberg | The 2010 tutorial is rather nice, though I still cannot compile its Lemma edivnP. The "rewrite -{1}(subnK le_dm) -addSn addnA -mulSnr" instruction breaks, maybe because mulSnr has changed its statement, or rewrite has changed its behavior. I have tried reading Sergey but he was too terse for me at the important points... | |
| Jul 12, 2015 at 9:25 | comment | added | Assia Mahboubi | Interesting: your answer made me realize I forgot the "seemingly" in my answer (now edited). For the time being, only a few tutorial-like references are available: An introduction to small scale reflection in Coq A.M. and G. Gonthier (2010, a bit outdated too); the material of a 2012 summer school; a recent course by Ilya Sergey, for a computer-oriented audience. | |
| Jul 12, 2015 at 9:14 | history | edited | Assia Mahboubi | CC BY-SA 3.0 |
Missing adjective
|
| Jul 11, 2015 at 18:12 | comment | added | darij grinberg | Thanks for the insider view! Do you know if there is a beginner-friendly introduction into the use of these libraries these days? I must admit I am glad to hear that the "cryptic boilerplate code" appears cryptic even to its authors and not just to me; but I would be really happy to be able to understand at least the non-too-technical parts of it. Is there something that is less fast-paced than the 2009 "tutorial" (also newer -- two of its examples don't compile anymore) and less technical than the Manual? | |
| Jul 11, 2015 at 17:30 | history | edited | David Roberts♦ | CC BY-SA 3.0 |
Fixed TeX/markdown
|
| Jul 11, 2015 at 17:16 | review | First posts | |||
| Jul 11, 2015 at 17:31 | |||||
| S Jul 11, 2015 at 17:12 | history | answered | Assia Mahboubi | CC BY-SA 3.0 | |
| S Jul 11, 2015 at 17:12 | history | made wiki | Post Made Community Wiki by Assia Mahboubi |