Codebase list cafeobj / v5.6b16+git20200131.1.261e3a5
Import upstream version 5.6b16+git20200131.1.261e3a5 Debian Janitor 2 years ago
4 changed file(s) with 19 addition(s) and 11 deletion(s). Raw diff Collapse all Expand all
22
33 - CITP is officially renamed to PTCalc
44 . but documents are not updated yet
5 - PTCalc(CITP) enhacements
5 - PTCalc(CITP) enhancements
66 . :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
88 - Search predicate enhancements
99 . nested search is properly handled
1010 . 'show path' accepts state specifier of the form 'depth-state'
3434 - xbin/cafeobj.in.in
3535 - make-cafeobj.lisp.in
3636
37 building for windows
38 --------------------
37 building using SBCL for windows
38 -------------------------------
3939 If Wine is installed, and within wine sbcl is installed, one can create
4040 a dump for Windows with
4141 ./configure --enable-windows
4242 make
4343 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
4553
4654
4755 building using ACL on Windows
4856 -----------------------------
4957 Building distribution tarballs on Windows using ACL requires a few more steps:
50 - configure CafeOBJ sources with
58 - configure CafeOBJ sources on Linux with
5159 ./configure
5260 no special argument is necessary.
5361 - 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
22 PortSystem 1.0
33
44 name cafeobj
5 version 1.5.9
5 version 1.6.0
66 categories lang
77 platforms linux
88 license BSD
1919 homepage http://cafeobj.org/
2020 master_sites http://cafeobj.org/files/${version}
2121
22 checksums rmd160 7116d2068e790820aae7e4d81efbed9691e03d65 \
23 sha256 a4085e9ee060a8a0a22cb7c522c17aa1ccadb5bdce8f90085e08ded3794498d4
22 checksums rmd160 908f9a80dc764892c2667af19df53323eb70bf5d \
23 sha256 ab97d3cf22d8556524c86540cbb11d4e2eb1ba38cb0198eb068a4493b745d560
2424
2525 depends_build bin:sbcl:sbcl
2626