search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
483 stars 85 forks source link

Literate programming ? #184

Open spitters opened 7 years ago

spitters commented 7 years ago

What is the status of literate programming in PG? I am aware of MMM

There is also this work based on PGIP and babel for emacs. There is probably more. Any insights?

Matafou commented 7 years ago

The only released tool that looks like literate programing I know of is coqdoc, and pg does not really support it. MMM is not supported anymore AFAIK. PGIP was never fully implemented and nobody is working on it anymore AFAIK. I never heard about a babel mode for pg but it would be interresting.

I know that Yann Regis-Gianas is developing a replacement tool for coqdoc but it is stalled I guess currently.