Import upstream version 5.6b16+git20200131.1.261e3a5
Debian Janitor
2 years ago
2 | 2 |
|
3 | 3 |
- CITP is officially renamed to PTCalc
|
4 | 4 |
. but documents are not updated yet
|
5 | |
- PTCalc(CITP) enhacements
|
|
5 |
- PTCalc(CITP) enhancements
|
6 | 6 |
. :init defined by :def is evaluated in the proof node to which it is applied
|
7 | |
. :init without substitution can be
|
|
7 |
. :init can be without substitution
|
8 | 8 |
- Search predicate enhancements
|
9 | 9 |
. nested search is properly handled
|
10 | 10 |
. 'show path' accepts state specifier of the form 'depth-state'
|
34 | 34 |
- xbin/cafeobj.in.in
|
35 | 35 |
- make-cafeobj.lisp.in
|
36 | 36 |
|
37 | |
building for windows
|
38 | |
--------------------
|
|
37 |
building using SBCL for windows
|
|
38 |
-------------------------------
|
39 | 39 |
If Wine is installed, and within wine sbcl is installed, one can create
|
40 | 40 |
a dump for Windows with
|
41 | 41 |
./configure --enable-windows
|
42 | 42 |
make
|
43 | 43 |
One can set the used wine prefix with WINEPREFIX. This creates already
|
44 | |
release ready .zip
|
|
44 |
release ready .zip (currently broken?).
|
|
45 |
|
|
46 |
Comments: 64bit version works, but it seems that the 32bit SBCL version
|
|
47 |
has problems running on a 64bit Wine. In this case:
|
|
48 |
- configure as usual with ./configure --with-lisp=sbcl on Linux
|
|
49 |
- move the files to Windows
|
|
50 |
- create dumps/sbcl/ directory
|
|
51 |
- run there in cmd.exe (not powershell!): sbcl < make-cafeobj.lisp
|
|
52 |
- use the CafeOBJ.exe from the dump/sbcl/ directory
|
45 | 53 |
|
46 | 54 |
|
47 | 55 |
building using ACL on Windows
|
48 | 56 |
-----------------------------
|
49 | 57 |
Building distribution tarballs on Windows using ACL requires a few more steps:
|
50 | |
- configure CafeOBJ sources with
|
|
58 |
- configure CafeOBJ sources on Linux with
|
51 | 59 |
./configure
|
52 | 60 |
no special argument is necessary.
|
53 | 61 |
- transfer the files to Windows
|
0 | |
cafeobj 675
|
1 | |
depends_build bin:sbcl:sbcl portdir lang/cafeobj description {New generation algebraic specification and programming language} homepage http://cafeobj.org/ epoch 0 platforms linux name cafeobj license BSD maintainers cafeobj.org:preining long_description {CafeOBJ is a language for writing formal (i.e. mathematical) specifications of models for wide varieties of software and systems, and verifying properties of them. CafeOBJ implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and doing proofs by executing the proof scores.} version 1.5.9 categories lang revision 0
|
|
0 |
cafeobj 692
|
|
1 |
depends_build {bin:sbcl:sbcl port:clang-3.4} portdir lang/cafeobj description {New generation algebraic specification and programming language} homepage http://cafeobj.org/ epoch 0 platforms linux name cafeobj license BSD maintainers cafeobj.org:preining long_description {CafeOBJ is a language for writing formal (i.e. mathematical) specifications of models for wide varieties of software and systems, and verifying properties of them. CafeOBJ implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and doing proofs by executing the proof scores.} version 1.6.0 categories lang revision 0
|
2 | 2 |
PortSystem 1.0
|
3 | 3 |
|
4 | 4 |
name cafeobj
|
5 | |
version 1.5.9
|
|
5 |
version 1.6.0
|
6 | 6 |
categories lang
|
7 | 7 |
platforms linux
|
8 | 8 |
license BSD
|
|
19 | 19 |
homepage http://cafeobj.org/
|
20 | 20 |
master_sites http://cafeobj.org/files/${version}
|
21 | 21 |
|
22 | |
checksums rmd160 7116d2068e790820aae7e4d81efbed9691e03d65 \
|
23 | |
sha256 a4085e9ee060a8a0a22cb7c522c17aa1ccadb5bdce8f90085e08ded3794498d4
|
|
22 |
checksums rmd160 908f9a80dc764892c2667af19df53323eb70bf5d \
|
|
23 |
sha256 ab97d3cf22d8556524c86540cbb11d4e2eb1ba38cb0198eb068a4493b745d560
|
24 | 24 |
|
25 | 25 |
depends_build bin:sbcl:sbcl
|
26 | 26 |
|