/[mojave]/metaprl/mk/config
ViewVC logotype

Log of /metaprl/mk/config

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 2518 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 11 23:49:50 1998 UTC (22 years, 7 months ago) by nogin
File length: 7399 byte(s)
Diff to previous 2508
Added -nostdinc -nostdinc++ options to CPP - we use cpp on .ml files
and there is no need to look into C/C++ include directories.


Revision 2508 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 19:01:22 1998 UTC (22 years, 8 months ago) by nogin
File length: 7377 byte(s)
Diff to previous 2498
Remove Makefile.dep on "make clean"


Revision 2498 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 02:19:13 1998 UTC (22 years, 8 months ago) by nogin
File length: 7364 byte(s)
Diff to previous 2497
- Nl_debug -> Mp_debug
- remove generated file theories/tptp/tptp_lex.ml on "make clean"


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


Revision 2495 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:25:01 1998 UTC (22 years, 8 months ago) by nogin
File length: 7333 byte(s)
Diff to previous 2468
mk/config:
 - OCAMLDEPFLAGS was overwritten here and all these "-prl" were not
   passed to ocamldep, so we were loosing lots of dependencies - fixed
 - When Makefile.dep is missing, it will be generated automatically.

README, doc/htmlman/mp-install.html
 - Now there is no need to call make depend before make


Revision 2468 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 14 22:47:05 1998 UTC (22 years, 9 months ago) by nogin
File length: 7265 byte(s)
Diff to previous 2466
Added the evaluator directory and moved there all the files left
from my first (unfinished) attempt to write an evaluator.

mk/config: $(ROOT)/lib should be the last include directory,
not the first one. This allows ocamldep to produce necessary
x.cmx: y.cmx dependencies.


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: 7265 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: 7068 byte(s)
Diff to previous 2459
More CAMLP4LIB changes


Revision 2459 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 8 23:54:29 1998 UTC (22 years, 9 months ago) by nogin
File length: 7864 byte(s)
Diff to previous 2453
Now make should work even if CAMLP4LIB environment variable is not defined.
Also, make clean should remove all filter/*.opt files.


Revision 2453 - (view) (download) (annotate) - [select for diffs]
Modified Sat Aug 29 18:46:42 1998 UTC (22 years, 9 months ago) by nogin
File length: 7801 byte(s)
Diff to previous 2440
Removed all references to "/usr/local/lib/nuprl-light" from the code


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: 7766 byte(s)
Diff to previous 2394
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 2394 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 3 03:13:54 1998 UTC (22 years, 10 months ago) by nogin
File length: 7724 byte(s)
Diff to previous 2376
Pass $(PROFILE) flag to gcc


Revision 2376 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 31 14:35:45 1998 UTC (22 years, 10 months ago) by jyh
File length: 7713 byte(s)
Diff to previous 2367
Added TPTP theory, and Ensemble library.  Fixed sequent displays.
BUG: rewrites fail on sequents.


Revision 2367 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 27 02:02:43 1998 UTC (22 years, 11 months ago) by nogin
File length: 7543 byte(s)
Diff to previous 2365
Use $(RM) instead of del or rm -f


Revision 2365 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 26 23:52:34 1998 UTC (22 years, 11 months ago) by nogin
File length: 7540 byte(s)
Diff to previous 2364
If CAMLLIB is not defined, use /usr/lib/ocaml


Revision 2364 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 26 23:00:29 1998 UTC (22 years, 11 months ago) by nogin
File length: 7490 byte(s)
Diff to previous 2345
Changed the default camlp4 directory to /usr/lib/camlp4


Revision 2345 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 23 04:33:00 1998 UTC (22 years, 11 months ago) by nogin
File length: 7496 byte(s)
Diff to previous 2344
Oops, forgot *.cmx


Revision 2344 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 23 04:31:04 1998 UTC (22 years, 11 months ago) by nogin
File length: 7490 byte(s)
Diff to previous 2342
Make "make clean" really clean - remove *.run *.cma and *.cmxa files


Revision 2342 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 23 03:20:30 1998 UTC (22 years, 11 months ago) by nogin
File length: 7471 byte(s)
Diff to previous 2336
Do not copy anything to the lib directory, use ln instead


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: 7449 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: 6503 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: 6503 byte(s)
Diff to previous 2314
Intermediate version with auto tactic.


Revision 2314 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 8 15:42:11 1998 UTC (22 years, 11 months ago) by jyh
File length: 6532 byte(s)
Diff to previous 2309
Pushed higherC into the refiner for efficiency.


Revision 2309 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 21:39:34 1998 UTC (22 years, 11 months ago) by jyh
File length: 6448 byte(s)
Diff to previous 2305
Working czf_itt_set.


Revision 2305 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 5 19:08:05 1998 UTC (22 years, 11 months ago) by nogin
File length: 6496 byte(s)
Diff to previous 2286
Compile with -noassert by default.
Compile without -noassert if DEBUG_NL environment variable is set.


Revision 2286 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 3 19:09:40 1998 UTC (22 years, 11 months ago) by nogin
File length: 6426 byte(s)
Diff to previous 2285
Added $(ROOT)/refiner/refsig/refine_error.h to the list
of the files *_verb.ml and *_simp.ml depend on.


Revision 2285 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 3 03:19:20 1998 UTC (22 years, 11 months ago) by nogin
File length: 6350 byte(s)
Diff to previous 2283
Allow changing the ocamlopt -inline option with the INLINE environment variable


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: 6325 byte(s)
Diff to previous 2274
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 2274 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 25 06:32:23 1998 UTC (23 years ago) by nogin
File length: 5631 byte(s)
Diff to previous 2265
Do not pass $(PROFILE) flag to $(OCAMLC)


Revision 2265 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 20 01:34:50 1998 UTC (23 years ago) by nogin
File length: 5649 byte(s)
Diff to previous 2260
OCAMLCPOPT allows to pass options to bytecode profiler


Revision 2260 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 17 19:38:58 1998 UTC (23 years ago) by jyh
File length: 5605 byte(s)
Diff to previous 2258
Did some profiling.


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


Revision 2251 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 16 16:26:27 1998 UTC (23 years ago) by jyh
File length: 5345 byte(s)
Diff to previous 2249
Added itt_test.


Revision 2249 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 16 07:33:35 1998 UTC (23 years ago) by nogin
File length: 5340 byte(s)
Diff to previous 2248
"make profile" seems to be working


Revision 2248 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 16 03:35:32 1998 UTC (23 years ago) by nogin
File length: 5337 byte(s)
Diff to previous 2209
Added OCAMLCP variable - if set to ocamlcp, make produces profiled code


Revision 2209 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 13:57:13 1998 UTC (23 years ago) by jyh
File length: 5294 byte(s)
Diff to previous 2201
Proving twice one is two.


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


Revision 2192 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 20:34:47 1998 UTC (23 years ago) by nogin
File length: 4546 byte(s)
Diff to previous 2190
Use cp -pf for copying %.mlz -> %.ml & %.mli


Revision 2190 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 13:48:44 1998 UTC (23 years ago) by jyh
File length: 4523 byte(s)
Diff to previous 2173
Updated the editor to use new Refiner structure.
ITT needs dform names.


Revision 2173 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 18 18:58:11 1998 UTC (23 years, 1 month ago) by nogin
File length: 4542 byte(s)
Diff to previous 2170
Use "cp -pf" instead of "install" to keep the timestamp
and prevent unnecessary recompiling.


Revision 2170 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 7 00:00:43 1998 UTC (23 years, 1 month ago) by nogin
File length: 4543 byte(s)
Diff to previous 2159
The right paths to prlc, ocamldep, etc in Makefiles


Revision 2159 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 29 14:50:25 1998 UTC (23 years, 1 month ago) by jyh
File length: 4525 byte(s)
Diff to previous 2156
Added ocaml_sos.


Revision 2156 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 28 18:31:05 1998 UTC (23 years, 1 month ago) by jyh
File length: 4528 byte(s)
Diff to previous 2151
ls() works, adding display.


Revision 2151 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 23 20:04:52 1998 UTC (23 years, 2 months ago) by jyh
File length: 4459 byte(s)
Diff to previous 2122
Initial rebuilt editor.


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: 4398 byte(s)
Diff to previous 2111
Added interactive proofs to filter.


Revision 2111 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 8 16:00:35 1998 UTC (23 years, 2 months ago) by jyh
File length: 4125 byte(s)
Diff to previous 2099
Use standard ocamldep.


Revision 2099 - (view) (download) (annotate) - [select for diffs]
Modified Fri Mar 20 22:16:22 1998 UTC (23 years, 3 months ago) by eli
File length: 4137 byte(s)
Diff to previous 2088
Eli: Changed integer parameters to Num.num's.


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: 4138 byte(s)
Diff to previous 2074
Initial ocaml semantics.


Revision 2074 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 12 22:28:17 1997 UTC (23 years, 7 months ago) by jyh
File length: 2881 byte(s)
Diff to previous 2061
Small changes for NT.


Revision 2061 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 8 15:02:40 1997 UTC (23 years, 9 months ago) by jyh
File length: 2866 byte(s)
Diff to previous 2047
This version compiles Ensemble.


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


Revision 2032 - (view) (download) (annotate) - [select for diffs]
Added Mon Apr 28 15:52:46 1997 UTC (24 years, 1 month ago) by jyh
File length: 2252 byte(s)
This is the initial checkin of Nuprl-Light.
I am porting the editor, so it is not included
in this checkin.

Directories:
    refiner: logic engine
    filter: front end to the Ocaml compiler
    editor: Emacs proof editor
    util: utilities
    mk: Makefile templates


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