[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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:

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.



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.

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.


Reply to: