/[mojave]
ViewVC logotype

Revision 2775


Jump to revision: Previous Next
Author: jyh
Date: Sun Jul 4 13:13:44 1999 UTC (22 years ago)
Changed paths: 243 (showing only 100; show all)
Log Message:
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.


Changed paths

Path Details
Directorymetaprl/Makefile modified , text changed
Directorymetaprl/editor/ml/Makefile modified , text changed
Directorymetaprl/editor/ml/mp.ml modified , text changed
Directorymetaprl/editor/ml/mp.mli modified , text changed
Directorymetaprl/editor/ml/mpconfig modified , text changed
Directorymetaprl/editor/ml/package_info.ml modified , text changed
Directorymetaprl/editor/ml/package_sig.mlz modified , text changed
Directorymetaprl/editor/ml/proof_edit.ml modified , text changed
Directorymetaprl/editor/ml/proof_edit.mli modified , text changed
Directorymetaprl/editor/ml/shell.ml modified , text changed
Directorymetaprl/editor/ml/shell_sig.mlz modified , text changed
Directorymetaprl/editor/ml/shell_state.ml modified , text changed
Directorymetaprl/filter/ modified , props changed
Directorymetaprl/filter/Makefile modified , text changed
Directorymetaprl/filter/base/ added
Directorymetaprl/filter/base/Files added
Directorymetaprl/filter/base/Makefile added
Directorymetaprl/filter/base/filter_ast.ml added
Directorymetaprl/filter/base/filter_ast.mli added
Directorymetaprl/filter/base/filter_buffer.ml added
Directorymetaprl/filter/base/filter_buffer.mli added
Directorymetaprl/filter/base/filter_cache.ml added
Directorymetaprl/filter/base/filter_cache.mli added
Directorymetaprl/filter/base/filter_cache_fun.ml added
Directorymetaprl/filter/base/filter_cache_fun.mli added
Directorymetaprl/filter/base/filter_comment.ml added
Directorymetaprl/filter/base/filter_comment.mli added
Directorymetaprl/filter/base/filter_debug.ml added
Directorymetaprl/filter/base/filter_debug.mli added
Directorymetaprl/filter/base/filter_exn.ml added
Directorymetaprl/filter/base/filter_exn.mli added
Directorymetaprl/filter/base/filter_grammar.ml added
Directorymetaprl/filter/base/filter_grammar.mli added
Directorymetaprl/filter/base/filter_hash.ml added
Directorymetaprl/filter/base/filter_hash.mli added
Directorymetaprl/filter/base/filter_html.ml added
Directorymetaprl/filter/base/filter_html.mli added
Directorymetaprl/filter/base/filter_magic.ml added
Directorymetaprl/filter/base/filter_magic.mli added
Directorymetaprl/filter/base/filter_ocaml.ml added
Directorymetaprl/filter/base/filter_ocaml.mli added
Directorymetaprl/filter/base/filter_prog.ml added
Directorymetaprl/filter/base/filter_prog.mli added
Directorymetaprl/filter/base/filter_summary.ml added
Directorymetaprl/filter/base/filter_summary.mli added
Directorymetaprl/filter/base/filter_summary_io.ml added
Directorymetaprl/filter/base/filter_summary_io.mli added
Directorymetaprl/filter/base/filter_summary_param.ml added
Directorymetaprl/filter/base/filter_summary_type.ml added
Directorymetaprl/filter/base/filter_summary_util.ml added
Directorymetaprl/filter/base/filter_summary_util.mli added
Directorymetaprl/filter/base/filter_type.ml added
Directorymetaprl/filter/base/filter_util.ml added
Directorymetaprl/filter/base/filter_util.mli added
Directorymetaprl/filter/base/free_vars.ml added
Directorymetaprl/filter/base/free_vars.mli added
Directorymetaprl/filter/base/infix.mli added
Directorymetaprl/filter/base/infix.pre.ml added
Directorymetaprl/filter/base/mLast_util.ml added
Directorymetaprl/filter/base/mLast_util.mli added
Directorymetaprl/filter/base/term_grammar.ml added
Directorymetaprl/filter/base/term_grammar.mli added
Directorymetaprl/filter/boot/ added
Directorymetaprl/filter/boot/Files added
Directorymetaprl/filter/boot/Makefile added
Directorymetaprl/filter/boot/conversionals_boot.ml added
Directorymetaprl/filter/boot/conversionals_boot.mli added
Directorymetaprl/filter/boot/exn_boot.ml added
Directorymetaprl/filter/boot/exn_boot.mli added
Directorymetaprl/filter/boot/proof_boot.ml added
Directorymetaprl/filter/boot/proof_boot.mli added
Directorymetaprl/filter/boot/proof_convert.ml added
Directorymetaprl/filter/boot/proof_convert.mli added
Directorymetaprl/filter/boot/proof_term_boot.ml added
Directorymetaprl/filter/boot/proof_term_boot.mli added
Directorymetaprl/filter/boot/rewrite_boot.ml added
Directorymetaprl/filter/boot/rewrite_boot.mli added
Directorymetaprl/filter/boot/sequent_boot.ml added
Directorymetaprl/filter/boot/sequent_boot.mli added
Directorymetaprl/filter/boot/tactic_boot.ml added
Directorymetaprl/filter/boot/tactic_boot.mli added
Directorymetaprl/filter/boot/tactic_boot_sig.mlz added
Directorymetaprl/filter/boot/tactic_type.ml added
Directorymetaprl/filter/boot/tactic_type.mli added
Directorymetaprl/filter/boot/tacticals_boot.ml added
Directorymetaprl/filter/boot/tacticals_boot.mli added
Directorymetaprl/filter/convert.ml added
Directorymetaprl/filter/convert.mli added
Directorymetaprl/filter/filter_ast.ml deleted
Directorymetaprl/filter/filter_ast.mli deleted
Directorymetaprl/filter/filter_bin.ml modified , text changed
Directorymetaprl/filter/filter_buffer.ml deleted
Directorymetaprl/filter/filter_buffer.mli deleted
Directorymetaprl/filter/filter_cache.ml deleted
Directorymetaprl/filter/filter_cache.mli deleted
Directorymetaprl/filter/filter_cache_fun.ml deleted
Directorymetaprl/filter/filter_cache_fun.mli deleted
Directorymetaprl/filter/filter_comment.ml deleted
Directorymetaprl/filter/filter_comment.mli deleted
Directorymetaprl/filter/filter_debug.ml deleted
[...]

  ViewVC Help
Powered by ViewVC 1.1.26