RFS: logiweb
Dear mentors,
I am looking for a sponsor for my package "logiweb".
* Package name : logiweb
Version : 0.2.0-1
Upstream Author : Klaus Grue <grue@diku.dk>
* URL : http://logiweb.eu/doc/0.2.0/download/debian.html
* License : GPL
Programming Lang: C
Description : a system for electronic distribution of mathematics
Section : math
It builds these binary packages:
logiweb - a system for electronic distribution of mathematics
The package appears to be lintian clean.
The upload would fix this bug: 543550
The package can be found on logiweb.eu:
http://logiweb.eu/doc/0.2.0/download/debian
I would be glad if someone would sponsor this package.
Bug 543550 is the ITP for logiweb. I have included
more info on logiweb below.
I have tried hard to get the package right, but
it is the first Debian package I have ever made.
Cheers,
Klaus
---
Long description:
Logiweb allows to web publish 'Logiweb pages', i.e.
journal quality articles which contain machine readable objects
like programs, testsuites, definitions, axioms, lemmas, and
proofs. Among other, Logiweb is suited for literate programming,
for publication of machine verified proofs, and for writing
proof checkers. Logiweb allows Logiweb pages to reference
previously published Logiweb pages such that programs on a page
may call programs on referenced pages, proofs on a page may
reference lemmas on referenced pages, and so on.
---
Logiweb was presented at MKM2003 (c.f. K.Grue: Logiweb, Mathematical
Knowledge Management Symposium 2003, Ed. Fairouz Kamareddine, Electronic
Notes in Theoretical Computer Science, Vol. 93, pp.70-101, 2004).
See also http://www.diku.dk/~grue/papers/logiweb/
It was also presented at the International Conference of Mathematical
Software ICMS2006 (c.f. K.Grue: Logiweb - A System for Web Publication of
Mathematics, In: Mathematical Software - ICMS 2006, Springer Berlin /
Heidelberg, Lecture Notes in Computer Science, Vol. 4151/2006, pp.343-353,
2006). See also http://www.diku.dk/~grue/papers/icms/icms.pdf
The latter paper was produced using Logiweb itself.
---
The 0.1.x beta test series of Logiweb was released 2006-2007. It was
tested by graduate students at the University of Copenhagen.
Based on the beta test, Logiweb has been ported from clisp to C and
has been cleaned up 2008-2009. The purpose of the 0.2.x pre-release
series is to test the C version and get packaging right. A 1.0.x series is
going to follow the 0.2.x series.
The 0.1.x beta test series followed a 0.grue.x alpha test series which was
released 2004-2006 and which was also tested by graduate students.
The design of Logiweb began in 1996, based on a previous system which
was used at the University of Copenhagen 1985-1996. That system in turn
built on a system that was developed 1972-1985.
Logiweb contains a regression testsuite with 15000+ small test cases
plus a number of larger test cases where the Logiweb compiler is applied
to a number of well- and ill-formed sources. The easiest way to get and
run the regression test is to use the .tar.gz version, c.f.
http://logiweb.eu/doc/0.2.0/download/gz.html.
Note that the main pages (http://logiweb.eu/ and the mirror sites
http://topps.diku.dk/logiweb/ and http://logiweb.imm.dtu.dk/) are
concerned with the 0.1.9 version of Logiweb and not relevant for the
present 0.2.0 release.
---
In the present version, Logiweb essentially consists of the "Logiweb
compiler" (lgc) and the Logiweb Abstract Machine (lgwam). The lgc compiler
translates sources expressed in the Logiweb Source language (lgs) to a
binary format. Thus, essentially, the present release of Logiweb is yet
another compiler for yet another programming language.
The lgs language is particularly suited to writing proof systems. But it
has also been used for other purposes. As an example, the lgc compiler
itself is written in its own language. Furthermore, software for a 'star
tracker' (c.f. http://en.wikipedia.org/wiki/Attitude_dynamics_and_control)
has been implemented in lgs for the European Space Agency as an experiment
in using literate programming for reducing cost of critical software. (for
'literate programming' see
http://en.wikipedia.org/wiki/Literate_programming).
The deep structures of the lgs language resembles those on Lisp. The
syntax is quite different. In lgs, the programmer defines the language he
or she wants to use in a header, and then uses that syntax in the body.
Through use of the macro expansion facilities and rendering capabilities,
the programmer can also define the semantics of lgs. So a determined
programmer can write in any language using lgs.
Programs written in lgs can reference libraries across the Internet in a
safe way. The output from the lgc compiler is in turn suited for web
publication by putting the output within reach of an http server (such as
Apache). This feature is the reason for the 'web' in 'Logiweb': the system
is suited for building a web of programs and of verified mathematics.
---
The main program of Logiweb is defined in the monolithic lgwam.c source
file. It may take some RAM to compile it. Actually, the built in
testsuite (the one with the 15000+ small test cases) may make gcc use
unreasonable amounts of memory, as reported at
http://gcc.gnu.org/bugzilla/show_bug.cgi?id=37448. Newer versions of gcc
seem to do well compiling lgwam.c, but the gcc bug is still open.
As mentioned, the lgc compiler is written in its own language. Actually,
lgc is the *only* compiler which can compile lgc. Hence, you cannot
compile lgc unless you have lgc already. For that reason, a binary version
of lgc is included in the distribution under the name 'pages.c'. The
pages.c file contains the binary version of the compiler run through the
'xxd -i' command. New versions of lgc are produced by compiling the new
version of lgc using the old version of lgc.
---
For more on Logiweb, see http://logiweb.eu/doc/0.2.0/index.html. Clicking
'Introduction' is a good place to start.
---END---
Reply to: