ViewVC logotype

Log of /metaprl/mk/preface

Parent Directory Parent Directory | Revision Log Revision Log

Sticky Revision:
(Current path doesn't exist after revision 6019)

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 3519 byte(s)
Diff to previous 3419
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).

Revision 3419 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 6 01:40:01 2001 UTC (19 years, 8 months ago) by nogin
File length: 3146 byte(s)
Diff to previous 3410
- I got rid of "MAKE_JOBS" variable in mk/config. If you want "make" to keep
running jobs in parallel when building MetaPRL, you should either
a) Make sure you have MAKEFLAGS environment variable contains appropriate "-j nn"
b) pass "-j nn" manually to make
c) Add "-j nn" to the MAKE_OPTS in mk/config (make will print warnings if you do this).

- I created a new config file - mk/config.local where people can put their
customized settings that do not belong to mk/config

- I fixed the problems caused by Camlp4 switch to keeping "escaped" strings
in the ASTs

- I got rid of the warnings caused by the outdated resource infos in old .prla

- I renamed back "Summary!parent2" -> "Summary!parent" and "Summary!resource2" ->
"Summary!resource" for backwards compatibility with old .prla and display forms.

Revision 3410 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 25 16:52:43 2001 UTC (19 years, 9 months ago) by nogin
File length: 3248 byte(s)
Diff to previous 3292
- Merged the Ocaml 3.02 changes

- Now http server is compiled in by default, but is only started if
the "-http true" argument is passed or MP_HTTP environment variable
is set to "true".

- A few other minor changes.

Revision 3292 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 24 10:25:49 2001 UTC (20 years ago) by nogin
File length: 3225 byte(s)
Diff to previous 3086
*** IMPORTANT: before doing "cvs update" see warning below ***

This commit implements a global resource that brings together resource management
that used to be done by each resource in its own way.

- A much simplier object (Mp_resource.resource_info) is now needed to create a new resource.
Additionally, many resource helper modules, such as term_match_table now provide functions
that create a resource_info for you.

- Funtions get_tactic_arg, get_int_tactic_arg, etc were replaced by a single function
get_resource_arg (note: functions for basci types, such as get_with_arg, get_sel_args, etc
were _not_ affected)

- Resource declaration statement now declares and resource creation statement now creates
a function get_<name>_resource. This function ca be passed as a second argument
to get_resource_arg to retrieve the current value of a particular resource.

- Resource annotation functions are now separate from the resource declaration/creation
mechanism. Resource annotation on a rule are now passed to a function named
process_<name>_resource_annotation. This function must have the appropriate
Mp_resource.annotation_processor type for the resource. This function can be declared
and implemented in _any_ module, not just the module that declares and creates the
<name> resource.

- Currenlty MetaPRL leaves it to Ocaml to keep track of these functions.
Consequently the module that defines the process_<name>_resource_annotation function
must be open'ed (not included!) by modules that use <name> annotations.


Unfinished business in this commit:
- Remainder of TODO 1.12 and 1.13

- Some proofs were broken by this commit. It appears that they were broken for
a "good" reason, but still need to be fixed.

- I need to make sure things now always have the right precedences (all things being equal,
the later an item is added to resource, the earlier precedence it should have).

- Consider adding refiner sentinels and display forms to global resource as well.
Currently each of them still does its own way of resource management (although the way
display forms are managed was changed by this commit - need to make sure the precedences
are right).

- Distributed refinement: I am afraid that the current resource code
will either work correctly only if all processes in the distributed group have
the same global resource, or it will attempt to pass around all the resource data.
Obviously, neither of these choices is a good one.

*** WARNING ***

This commit changes the tactic_arg type and also makes minor changes in
the FilterCache.info type. Because of that old .prlb and .cmoz files
*will no longer work*. Old .prla files will work, but will produce lots
of (harmless) Filter_summary.dest_term warning.

Before doing "cvs update" do the following:
1) export all your unsaved proofs into .prla files.
2) rm -f theories/*/*.prlb
3) run "make clean"

Revision 3086 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 22 20:58:58 2000 UTC (20 years, 8 months ago) by nogin
File length: 3225 byte(s)
Diff to previous 3059
1) Proved some *Formation rules that used to be primitive (using in part
Alexei's cut rule idea). We should probably continue this job and
eliminate "primitiveness" from as much Formation rules as we can.

2) unitSqequal rule should be primitive

3) mk: don't pass -j1 to make when MAKE_JOBS = 1

4) In MP toploop, when a non-negatice integer is found where
an address was expected, that integer is considered to be
the hypothesis number. This enables applying primitive rules
from the MP toploop.

Revision 3059 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 11 00:31:56 2000 UTC (20 years, 9 months ago) by nogin
File length: 3163 byte(s)
Diff to previous 3032
MetaPRL now requires an extra patch to by applied to Camlp4 -
Jason's Plexer patch.

The new camlp4 RPM that contains the patch is available at
ususal places.

Revision 3032 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 25 23:10:51 2000 UTC (20 years, 11 months ago) by jyh
File length: 3133 byte(s)
Diff to previous 3030
Fixed the problem with loading and editing several theories that have common

Fixed a problem with bytecode make forgetting to do things in filter.

Revision 3030 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 25 17:22:43 2000 UTC (20 years, 11 months ago) by nogin
File length: 3071 byte(s)
Diff to previous 3029
TODO - ocamldebug and ocamlprof support.

Revision 3029 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 21 00:58:24 2000 UTC (20 years, 11 months ago) by jyh
File length: 3034 byte(s)
Diff to previous 2994
Added readline input handling.

Revision 2994 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 30 03:55:15 2000 UTC (21 years ago) by nogin
File length: 2896 byte(s)
Diff to previous 2890
I wrote several sections of MetaPRL Developer Guide.

Please take a look at it at

Revision 2890 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 18 04:30:36 2000 UTC (21 years, 4 months ago) by nogin
File length: 2900 byte(s)
Diff to previous 2889
Restored the old code for proving the propositional pigeon-hole principle.
For some reason the proveT tactic does not get exported properly,
so p4.ml still does not work.

Revision 2889 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 18 03:26:38 2000 UTC (21 years, 4 months ago) by nogin
File length: 2861 byte(s)
Diff to previous 2864
- When compiling a MetaPRL file referenced using its path instead of
just a name, only the basename is now used as the theory name.
This allowed me to put some MetaPRL files into a separate directory
without having to give them their own Makefile and still be able
to cd the theories produced by those files.
However, that "separate directory" still has to be added to the
include pacth (using the -I command) in order for this to work.

- Added a new mk/config variable TESTS that specifies whether to compile
various test theories (itt_test, test, prop-pigeon) into MetaPRL.
By default it is set to "no".

- Added the prop-pigeon theory and put the pigeon2 - pigeon9 theorems there.
I still have to recover pigeonT from the CVS repository and fix propDecideT
to be able to test these.

Revision 2864 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 29 02:57:22 1999 UTC (21 years, 6 months ago) by nogin
File length: 2600 byte(s)
Diff to previous 2860
Both Caml 2.04 and 2.03 may be used to compile MetaPRL

Revision 2860 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 22 06:11:47 1999 UTC (21 years, 7 months ago) by nogin
File length: 2595 byte(s)
Diff to previous 2859
"ocamlmktop -v" bug workaround.

It turned out that "ocamlmktop -v" was not only printing the version number,
but also creating an a.out file with Ocaml toploop. After this fix, it is going
to put that toploop into /dev/null ...

Revision 2859 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 22 05:43:56 1999 UTC (21 years, 7 months ago) by nogin
File length: 2570 byte(s)
Diff to previous 2858
Made MetaPRL compatible with ocaml-2.03/camlp4-2.03

At the same time it became incompatible with ocaml-2.02/camlp4-2.02...

Revision 2858 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 22 00:42:26 1999 UTC (21 years, 7 months ago) by nogin
File length: 2570 byte(s)
Diff to previous 2775
Added a check that makes sure that a correct version of Ocaml and Camlp4
is used.

Revision 2775 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 1838 byte(s)
Diff to previous 2747
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:

       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.

Revision 2747 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 23:40:57 1999 UTC (22 years ago) by nogin
File length: 1673 byte(s)
Diff to previous 2743
By default, run make with -s (silent) flag.

This way you are able to see all the essential messages that otherwise
would get lost among all those ocamlc & ocamlopt commands

Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 1621 byte(s)
Diff to previous 2722
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).


Revision 2722 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 17 09:11:00 1999 UTC (22 years ago) by eli
File length: 1621 byte(s)
Diff to previous 2663
Added CAMLP4MACRO to be used instead of CPP.

Revision 2663 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 21 01:37:22 1999 UTC (22 years, 1 month ago) by nogin
File length: 1622 byte(s)
Diff to previous 2661
I tagged the current version with meta-prl-0_5_2 tag and bumped the version number
to 0.5.3

Revision 2661 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 21 01:22:28 1999 UTC (22 years, 1 month ago) by nogin
File length: 1622 byte(s)
Diff to previous 2640
- Updated the BUGS file

Changes suggested by Carl R. Witty <cwitty@newtonlabs.com>:
- Give better error message when $(OSTYPE) is unknown
- Added comments to mk/config telling that the file is generated

Revision 2640 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 8 16:13:40 1999 UTC (22 years, 2 months ago) by nogin
File length: 1462 byte(s)
Diff to previous 2637
Updated the .prlb files.

There is some bootstrapping issue here - I had to copy .cmoz to .prlb
and recompile three times before they stopped changing.

Revision 2637 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 6 23:29:52 1999 UTC (22 years, 2 months ago) by nogin
File length: 1462 byte(s)
Diff to previous 2633
Added ENSROOT and OCAMLSRC to mk/config.

When the mk/config is created for the first time, the environment
variables would be consulted and if they point to existing directories,
they would be added to mk/config, otherwise "undefined" is used.

Once ENSROOT and OCAMLSRC are entered into mk/config,
make would ignore ENSROOT and OCAMLSRC environment variables

Revision 2633 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 5 21:16:49 1999 UTC (22 years, 2 months ago) by nogin
File length: 1376 byte(s)
Diff to previous 2621
I've created a tag "meta-prl-0_5", bumped the version number to 0.5.1
and moved the vesrion number from editor/ml/Makefile to mk/preface

Revision 2621 - (view) (download) (annotate) - [select for diffs]
Modified Fri Mar 19 06:18:45 1999 UTC (22 years, 3 months ago) by nogin
File length: 1358 byte(s)
Diff to previous 2590
Working on MetaPRL portability.

clib - fixed some gcc-isms

refiner - some C preprocesseors do not like if in "-I<directory>" option
   -I and <directory> are separated by a space - fixed

mk - C compiler is now defined in mk/config, gcc is used by default

mk/rules - some gcc-specific preprocessor options are used only when CC equals
   gcc, some Solaris-specific cpp options are used when CC!=gcc and OSLEVEL=

mk/rules - when OSLEVEL=solaris, we have to compile libposix4 along with
   libpthread, on Linux we only need libpthread and on all other systems,
   make should print an error message

With these changes I was able to compile bytecode MetaPRL with pthreads
on Solaris using either cc or gcc, but native code MetaPRL still would not

Revision 2590 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 12 23:50:37 1999 UTC (22 years, 4 months ago) by nogin
File length: 1320 byte(s)
Diff to previous 2582
Added the Linear_set implementation based on arrays (the same as was used
before). Somehow it still made things a little bit faster, I have no idea why.

Added the new compile-time option into mk/config file that allows to choose
which Linear_set implementation to use. All relevant comments will be added
to your mk/config file automatically when you ran make for the first time
after "cvs update"

Revision 2582 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 2 01:54:59 1999 UTC (22 years, 4 months ago) by nogin
File length: 1246 byte(s)
Diff to previous 2580
- Now all user configuration options are in mk/config file
- The old mk/config file (the one with all the make rules)
  is now called mk/rules, the new mk/config is _not_ on CVS
- When mk/config.init is newer than mk/config (e.g. mk/config
  does not exist), mk/config.init is appended to mk/config
- Toplevel Makefile checks if mk/config definies everything
  it should define and prints an error message if not

- Fixed a bug in refiner/refsig/refine_error.h that prevented
  SIMPLE refiner from being built

- I was not able to completely check if everything works because
  of the bug introduced by the previous check-in

Revision 2580 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jan 31 21:42:08 1999 UTC (22 years, 4 months ago) by jyh
File length: 1100 byte(s)
Diff to previous 2535
Added "simp" and "verb" rules to Makefiles.  There are no *.mlp and *.mlip
files in the refiner any longer.  Instead, the C-preprocessor is run at
compile time.

By default, the verbose refiner is generated.  To get the others, use
make simp, or make opt_simp.

Revision 2535 - (view) (download) (annotate) - [select for diffs]
Modified Thu Dec 31 02:02:48 1998 UTC (22 years, 5 months ago) by nogin
File length: 922 byte(s)
Diff to previous 2497
Fixed the bytecode profiling build.

Since ocamlcp does not allow threads,
the profiled bytecode is compiled without the -thread option

Revision 2497 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:52:18 1998 UTC (22 years, 8 months ago) by nogin
File length: 938 byte(s)
Diff to previous 2466
Renaming it in Makefiles:

Revision 2466 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 14 03:45:59 1998 UTC (22 years, 9 months ago) by nogin
File length: 938 byte(s)
Diff to previous 2461
Enabled profiled build under Ocaml 2.00.

Ocaml 2.00 has a bug (profiled code woul segfault), so
you need to use my patched version of ocaml: ocaml >= 2.00-4
I've installed ocaml-2.00-4 on Mojave.

Revision 2461 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 9 00:36:55 1998 UTC (22 years, 9 months ago) by nogin
File length: 825 byte(s)
Diff to previous 2047
More CAMLP4LIB changes

Revision 2047 - (view) (download) (annotate) - [select for diffs]
Added Wed Aug 6 16:18:55 1997 UTC (23 years, 10 months ago) by jyh
File length: 355 byte(s)
This is an ocaml version with subtyping, type inference,
d and eqcd tactics.  It is a basic system, but not debugged.

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26