search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

Further Ubuntu packages #803

Closed sternk closed 10 years ago

sternk commented 10 years ago

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

sternk commented 10 years ago

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 commented 10 years ago

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 commented 10 years ago

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

sternk commented 10 years ago

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 commented 10 years ago

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 commented 10 years ago

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 commented 10 years ago

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

Reduce working with Hets Test file used:

sternk commented 10 years ago

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 commented 10 years ago

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 commented 10 years ago

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 commented 10 years ago

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

How do I install these packages?

sternk commented 10 years ago

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

Ah, it's the "hets" package.