Groups | Search | Server Info | Login | Register


Groups > comp.programming.literate > #80

ProofPower

From dtopham <dtopham@gmail.com>
Newsgroups comp.programming.literate
Subject ProofPower
Date 2014-12-21 14:32 -0500
Organization albasani.net
Message-ID <m7777n$ff9$1@labrador.cs.tufts.edu> (permalink)
References <sfid-H-20141221-143203-+23.59-1@multi.osbf.lua>

Show all headers | View raw


I recently discovered this great program that includes support for literate programming. Very nicely done! Although focused on SML and proofs, it has ability to be extended to other languages:

Rob, I am really enjoying learning about ProofPower and so impressed at the amount of documentation and extra facilities that I didn't even know were part of this program.  e.g. I have long been interested in "literate programming" and find your approach using =SML and =TEX to be very efficient. I read in the usr001.pdf that it is possible to add other languages such as =C but don't quite see what I have to do to make that work.  I tried just putting =C followed by the some C code, but got errors from docsml that say =C is not defined.
The example is from page 56 in the section about sieve so I imagine the info is there somewhere, but I find that section a bit difficult for me at this early stage of learning about ProofPower. I found I can use =DUMP to get a similar effect, however in the document =C would certainly be more descriptive.
-Dave
p.s. I am cc'ing the literate programming group to this discussion because I think there may be others that do not know about ProofPower and its support for literate programming.

Back to comp.programming.literate | Previous | Next | Find similar


Thread

ProofPower dtopham <dtopham@gmail.com> - 2014-12-21 14:32 -0500

csiph-web