Further Ubuntu packages

[sternk]

Reported by till and assigned to cprodescu
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803

---

• hets-isabelle
  • polyml http://www.polyml.org/
  • isabelle2009-1 and Proof General (including HOL-Complex, HOLCF...) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
• hets-lf
  • ml
  • twelf http://twelf.plparty.org/wiki/Main_Page (ask Florian Rabe)
• hets-cas
  • reduce http://www.reduce-algebra.com/ (ask Dominik Dietrich)
• hets-maude
  • maude http://maude.cs.uiuc.edu/ (full Maude is needed, ask Mihai)

[sternk]

Comment by cprodescu
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:2

---

__*
isabelle-2009-2 done... I have uploaded it on a temporary PPA (ppa:cprodescu/latexml), as I have to remove a broken source (for the same isabelle) that I have uploaded to the Hets PPA.
It has the Pure and HOL logics pre-compiled and supports the proofgeneral GUI.

[sternk]

Comment by till
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:3

---

Here some info for Twelf (step 1 should be sufficient for us):

0) install Twelf
   - install SMLNJ http://www.smlnj.org/
   - check out Twelf https://cvs.concert.cs.cmu.edu/twelf/branches/twelf-mod
   - compile Twelf using
     sml build\twelf-server-smlnj.sml
   - check by running twelf-server.bat or twelf-server

1) install jEdit 4.3

2) set up Twelf mode
   - add lf.xml to jEdit modes directory
   - add entry to catalog file in same directory
   - see here for example https://svn.kwarc.info/repos/kwarc/rabe/Program_Data/jEdit/modes

3) set up Twelf macros
   - add twelf.bsh to jEdit macros directory
   - add twelf-paths.template to jEdit macros direcory, rename to twelf-paths, adjust paths in it
   - see here for example https://svn.kwarc.info/repos/kwarc/rabe/Program_Data/jEdit/macros

4) run Twelf macro to type-check the current file and display Twelf output
   - use Macro menu
   - or set shortcut in Global Options/Shortcuts

5) configure OMDoc output
   set doOMDoc to false in twelf-paths if you do not want to produce OMDoc files

6) configure Unicode for UTF8-encoded elf files
   - install a Unicode font, e.g., GNU unifont http://unifoundry.com/unifont.html
   - switch to that font in jEdit
   - set up jEdit abbreviations to conveniently input Unicode
     see here for example https://svn.kwarc.info/repos/kwarc/rabe/Program_Data/jEdit/abbrevs

[sternk]

Comment by cprodescu
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:4

---

• Twelf - 1.5R3r1687 packaged and uploaded to the ppa.
• About REDUCE:
  which version should I compile (psl or csl?). I've got them both working, but I need some test procedures (test files + how should I test it with hets).

[sternk]

Comment by till
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:5

---

Replying to cprodescu:

• Twelf - 1.5R3r1687 packaged and uploaded to the ppa.
• About REDUCE:

which version should I compile (psl or csl?). I've got them both working, but I need some test procedures (test files + how should I test it with hets).

Dominik, can you answer this?

[sternk]

Comment by till
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:6

---

Replying to cprodescu:

• Twelf - 1.5R3r1687 packaged and uploaded to the ppa.
• About REDUCE:

which version should I compile (psl or csl?). I've got them both working, but I need some test procedures (test files + how should I test it with hets).

Dominik, can you answer this?

[sternk]

Comment by maeder
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:7

---

both, see user guide (10.6)

This is a connection to the computer algebra system from
\url{http://www.reduce-algebra.com/}. Installation is possible as follows:

\begin{verbatim}
svn co https://reduce-algebra.svn.sourceforge.net/svnroot/reduce-algebra
cd reduce-algebra/trunk
./configure --with-csl --with-psl
make
\end{verbatim}

The binary \texttt{redcsl} will be searched in the \texttt{PATH} or is taken
from the \texttt{HETS\_REDUCE} environment variable.

[sternk]

Comment by cprodescu
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:8

---

Reduce working with Hets
Test file used:

• hets -g -A Hets/CSL/TestData/reduceTest.het

[sternk]

Comment by cprodescu
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:9

---

Reduce version 04-Aug-10 packaged and published on the Hets PPA.
Successfully tested with the currently packaged version of Hets (hets -g trunk/CSL/TestData/reduceTest.het)

[sternk]

Comment by cprodescu
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:10

---

Any test files for Maude ? (And how should I actually test it with Hets)

[sternk]

Comment by till
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:11

---

Replying to cprodescu:

Any test files for Maude ? (And how should I actually test it with Hets)

Mihai, can you answer this?

[sternk]

Comment by maeder
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:13

---

How do I install these packages?

[sternk]

Comment by maeder
Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/803#comment:14

---

Ah, it's the "hets" package.