/[mojave]/metaprl/mllib/Makefile
ViewVC logotype

Log of /metaprl/mllib/Makefile

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 2520 - (view) (download) (annotate) - [select for diffs]
Modified Sun Nov 29 23:28:38 1998 UTC (22 years, 6 months ago) by nogin
File length: 1055 byte(s)
Diff to previous 2497
Added the bi-directional Term_copy module
written by Yegon Bryukhov <yegor@lpcs.math.msu.ru>

This version is undebugged and is very slow:
it seems to be quadratic and also it becomes much slower
after each invocation.


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: 1066 byte(s)
Diff to previous 2494
Renaming it in Makefiles:
NLLIB -> MPLIB, NLFILES -> MPFILES, NL2FILES -> MP2FILES, etc.


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 1066 byte(s)
Diff to previous 2443
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2443 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 24 13:43:48 1998 UTC (22 years, 10 months ago) by jyh
File length: 1066 byte(s)
Diff to previous 2442
Slightly better Ensemble scheduling.
Native-code compiler has trouble marshaling functions--
its probably a problem with the marshaler.

Added Nl_num, a ML-only implementation of bignums.
This is slower than the C version used by OCaml, but
we can marshal the Nl_nums.  Most of the files changed
are just replacements of Num.* with Nl_num.*.


Revision 2442 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 21 22:22:55 1998 UTC (22 years, 10 months ago) by jyh
File length: 1028 byte(s)
Diff to previous 2440
Added distributed refinement using Ensemble.
This is an initial version.  The scheduler needs some performance
tuning, and Ensemble needs a little work on blocking IO.

By default, Ensemble support is not compiled into Nuprl-Light.
To enable distributed refinement, you need a copy of Ensemble,
which is available at:

    http://www.cs.cornell.edu/Info/Projects/Ensemble/

When Ensemble is installed, set the environment variable
ENSROOT to the root Ensemble directory.  On mojave, I've precompiled
a version of Ensemble in ~jyh/nuprl/src/ensemble.  Once this
variable is set, make will build the distributed refiner.

Ensemble uses a separate "gossip" daemon to get processes to form groups.
The program editor/ml/nlgossip starts this daemon.  Once the daemon
is started, multiple copies of nl will know about each other, and ship
refinement jobs to each other.  So if you want faster refinement, start
multiple copies of nl.  These copies can be started and killed at
any time; Ensemble provides support for failure detection and recovery.


Revision 2440 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 17 15:28:26 1998 UTC (22 years, 10 months ago) by jyh
File length: 868 byte(s)
Diff to previous 2436
Added multithreaded refinement.  NOTE: this requires a patch to
LinuxThreads.  The patched library is in clib/libpthreads-i386-linux.lib.
I'll add the source level patch in the next release.

Removed failure caching from tptp_prove to get more deterministic
refinements.  Modified Tptp_prove.testT to create a single proof
goal, rather than running proveT several times.


Revision 2436 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 10 18:14:53 1998 UTC (22 years, 10 months ago) by nogin
File length: 856 byte(s)
Diff to previous 2435
We used to have S (Set) module signature defined in Splay_set.
Now I added a new file for that.


Revision 2435 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 10 18:01:28 1998 UTC (22 years, 10 months ago) by nogin
File length: 847 byte(s)
Diff to previous 2433
Since Fun_splay_set in much faster than Splay_set
and Red_black_set is even faster, there is no reason
to keep Splay_set


Revision 2433 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 10 17:19:03 1998 UTC (22 years, 10 months ago) by jyh
File length: 859 byte(s)
Diff to previous 2417
Added red-black set implementation.


Revision 2417 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 6 22:11:58 1998 UTC (22 years, 10 months ago) by jyh
File length: 815 byte(s)
Diff to previous 2408
Yet another fix to unification.  Changes have not been added to
term_std.  There is a problem with delayed free_var computation
in term_ds.  Patched it temporarily.


Revision 2408 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 5 03:22:01 1998 UTC (22 years, 10 months ago) by nogin
File length: 803 byte(s)
Diff to previous 2407
A useful tool for debugging new implementations of Set module


Revision 2407 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 5 01:12:22 1998 UTC (22 years, 10 months ago) by jyh
File length: 783 byte(s)
Diff to previous 2401
Added util String_set module.
Unification now used String_set.StringSet for the constants (Term_ds
still uses its own StringSet).
Modified sequent display.
Added Shell.goal () to the the current proof goal.


Revision 2401 - (view) (download) (annotate) - [select for diffs]
Modified Tue Aug 4 16:49:19 1998 UTC (22 years, 10 months ago) by jyh
File length: 770 byte(s)
Diff to previous 2391
Added somewhat functional splay sets.


Revision 2391 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 2 23:38:49 1998 UTC (22 years, 10 months ago) by jyh
File length: 742 byte(s)
Diff to previous 2336
Added splay_tables, which act like functional hash tables over
an ordered type.  This code is derived from Splay_set.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 11 months ago) by jyh
File length: 728 byte(s)
Diff to previous 2333
Added NL toploop so that we can compile NL native code.


Revision 2333 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 17 15:39:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 725 byte(s)
Diff to previous 2325
CZF is complete, although we may wish to add pairing and inf.


Revision 2325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 14 15:44:03 1998 UTC (22 years, 11 months ago) by jyh
File length: 737 byte(s)
Diff to previous 2307
Intermediate version with auto tactic.


Revision 2307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 17:55:31 1998 UTC (22 years, 11 months ago) by nogin
File length: 712 byte(s)
Diff to previous 2303
Removed $Log messages from all NL files.


Revision 2303 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 5 06:52:16 1998 UTC (22 years, 11 months ago) by nogin
File length: 706 byte(s)
Diff to previous 2283
Better Makefiles


Revision 2283 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 2 18:38:08 1998 UTC (22 years, 11 months ago) by jyh
File length: 694 byte(s)
Diff to previous 2272
Refiner modules now raise RefineError exceptions directly.
Modules in this revision have two versions: one that raises
verbose exceptions, and another that uses a generic exception.


Revision 2272 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 23 22:12:44 1998 UTC (23 years ago) by jyh
File length: 687 byte(s)
Diff to previous 2258
Improved rewriter speed with conversion tree and flist.


Revision 2258 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 17 15:46:02 1998 UTC (23 years ago) by jyh
File length: 679 byte(s)
Diff to previous 2221
Optimizing compiler.


Revision 2221 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 7 01:08:40 1998 UTC (23 years ago) by nogin
File length: 660 byte(s)
Diff to previous 2201
Use the sets implementation based on the splay trees in Term_ds module
This implementation is based on the splay trees code taken from TAL typechecker


Revision 2201 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 29 14:53:34 1998 UTC (23 years ago) by jyh
File length: 648 byte(s)
Diff to previous 2152
Better Makefiles.


Revision 2152 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 24 02:44:07 1998 UTC (23 years, 2 months ago) by jyh
File length: 513 byte(s)
Diff to previous 2122
Added more extensive debugging capabilities.


Revision 2122 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 13 21:11:25 1998 UTC (23 years, 2 months ago) by jyh
File length: 501 byte(s)
Diff to previous 2108
Added interactive proofs to filter.


Revision 2108 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 8 15:08:37 1998 UTC (23 years, 2 months ago) by jyh
File length: 489 byte(s)
Diff to previous 2107
Moved precedence to mllib.


Revision 2107 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 8 14:57:37 1998 UTC (23 years, 2 months ago) by jyh
File length: 476 byte(s)
Diff to previous 2093
ImpDag is in mllib.


Revision 2093 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 23 14:46:44 1998 UTC (23 years, 4 months ago) by jyh
File length: 450 byte(s)
Diff to previous 2088
First implementation of binary file compilation.


Revision 2088 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 18 18:48:05 1998 UTC (23 years, 4 months ago) by jyh
File length: 434 byte(s)
Diff to previous 2047
Initial ocaml semantics.


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: 354 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