/[mojave]/metaprl/editor/ml/Makefile
ViewVC logotype

Log of /metaprl/editor/ml/Makefile

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: 5933 byte(s)
Diff to previous 3410
- 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 3410 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 25 16:52:43 2001 UTC (19 years, 8 months ago) by nogin
File length: 6083 byte(s)
Diff to previous 3066
- 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 3066 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 19 22:18:30 2000 UTC (20 years, 9 months ago) by nogin
File length: 6083 byte(s)
Diff to previous 3064
- Ocamldep now treats "derive" in the same way as "include" and "open"
(instead of just ignoring it) which recovered some missing dependencies
in the FOL theory.

- Better TeX dependencies, including "make tex" now noticing when
a theory changes.

- Section hack - now Index and Bibliography are created as normal section
(without two separate "Index" headings as it used to be).


Revision 3064 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 19 06:36:31 2000 UTC (20 years, 9 months ago) by nogin
File length: 6017 byte(s)
Diff to previous 3057
Documentation Makefiles hacking:
- Added "texbyte and texopt" in edimor/ml to force using byetcode/native code
MetaPRL for generating TeX files. "make tex" would use opt if available
and bytecode otherwise.

- More dependencies to make sure the files are being regenerated as necessary.


Revision 3057 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 18:26:37 2000 UTC (20 years, 9 months ago) by jyh
File length: 5768 byte(s)
Diff to previous 3036
This jumbo update is a documentation update.  There are no
logical changes.  I did two things:

1. First, comments that begin with the sequence "(*!" are
   interpreted as structured comments.  The contents are parsed
   as terms, and the comments will display in the editor window.
   The comments may contain arbitrary text, as usual, and they
   can also contain explicit terms.  The syntax for terms is:

   @opname[p1, ..., pn]{t1; ...; tm}

   or there is an alternate syntax:

   @begin[opname, p1, ..., pn]
   arg
   @end[opname]

   Text sequences count as a single term.  So, for instance, the
   term @bf{Hello world} display the "Hello world" text in a bold
   font.

   The "doc" term is used for text that is considered to be
   documentation.  There is a set of LaTeX-like terms that you can
   use to produce good-looking documentation.  These are all
   documented in the theories/tactic/comment.ml module.  The exact
   syntax of structured comments is defined in the
   mllib/comment_parse.mll file.  You can also look at any of the
   module in the theories/itt directory if you want to see examples.

   You can generate a pritable version of documentation with the
   print_theory command in the editor.  For example, the command

   # print_theory "itt_equal";;

   produces a file called output.tex that can be formatted with
   your favorite version of latex2e.  You can also generate a
   manule of all the theories by running "make tex" in the
   editor/ml directory.  Or you can run "make" in the
   doc/latex/theories directory.

   The files are hyperlinked, and they contain a table of contents
   and an index.  The preferred reader is acrobat, and the preferred
   formatter is pdflatex.

2. Second, I documented the tactic, base, itt, and czf theories.

3. Oh, and I also added a spelling checker:)  You can turn on the
   spelling checker with the -debug spell option or MP_DEBUG=spell.
   If prlc thinks that your files contain spelling mistakes, it will
   print them out and abort.  You can fix this problem by 1) fixing
   the spelling error, 2) adding the words withing a @spelling{words}
   term in a comment, or adding the words to you .ispell_english
   directory.

   For example, we could either do this:

   @begin[spelling]
   Aleksey Nogin
   @end[spelling]

   Or we could just add Alexey to either $cwd/.ispell_english, or
   ~/.ispell_english.

   The spell checker uses /usr/dict/words as a database, which it
   compiles to a hashtable in /tmp/metaprl-spell-$USER.dat.  Don't
   worry about the tmp file, it is generated automatically.


Revision 3036 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 27 19:55:54 2000 UTC (20 years, 10 months ago) by nogin
File length: 5478 byte(s)
Diff to previous 3029
- Fixed the problem with leaking attributes.

- Fixed the problem with top-level functions (such as clean_all)
removing the "Primivive" flag and replacing it with "Interactive".

- Fixed some display forms.

- Removed "empty" .prla files in ITT and "refreshed" the rest of them.

- More in BUGS and TODO.

- Other small changes.


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: 5470 byte(s)
Diff to previous 3014
Added readline input handling.


Revision 3014 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 13 06:16:19 2000 UTC (21 years ago) by nogin
File length: 5368 byte(s)
Diff to previous 2980
I wrote a proof tree normalization that tries to eliminate unnecessary nodes
in the proof tree and makes "deep" proof browsing much more
plesent.

Currently this is probably a little inefficient since it' too eager and
the results are not always saved. To fix this, we'll need to make Tactic_boot extracts
mutable so that we could do normalization (and other operations) properly lazily.

Other small changes.


Revision 2980 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 17 07:12:16 2000 UTC (21 years, 1 month ago) by nogin
File length: 5358 byte(s)
Diff to previous 2922
Small step towards making bytecode profiling more automatic.


Revision 2922 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 16 19:52:02 2000 UTC (21 years, 3 months ago) by lolorigo
File length: 5343 byte(s)
Diff to previous 2899
added/improved functionality for metaprl/jprover/nuprl5 io


Revision 2899 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 21 00:04:25 2000 UTC (21 years, 4 months ago) by nogin
File length: 5233 byte(s)
Diff to previous 2889
- Fixed the prop-pigeon tactics.
The solution was to wrap dT with thinningT false

- Added the test files for all the prop-pigeon test we are using.

- Made sure "make clean" in editor/ml also cleans editor/ml/tests


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: 5167 byte(s)
Diff to previous 2888
- 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 2888 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 18 01:01:54 2000 UTC (21 years, 4 months ago) by nogin
File length: 5018 byte(s)
Diff to previous 2775
Moved all the test files to the tests directory to keep things cleaner


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: 5000 byte(s)
Diff to previous 2763
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.


Revision 2763 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 29 03:40:34 1999 UTC (21 years, 11 months ago) by nogin
File length: 5882 byte(s)
Diff to previous 2744
Removed -I $(ROOT)/lib from the INCLUDES.
It was unnecessary since mk/rules adds -I $(ROOT)/lib to ocaml{c,opt} calls anyway.


Revision 2744 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 18:45:15 1999 UTC (22 years ago) by nogin
File length: 5899 byte(s)
Diff to previous 2743
Fixed couple of typos that prevented "make opt" from working


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (22 years ago) by jyh
File length: 5845 byte(s)
Diff to previous 2666
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.

Changes:
   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
      otherwise.

   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).

Jason


Revision 2666 - (view) (download) (annotate) - [select for diffs]
Modified Sat May 22 01:28:28 1999 UTC (22 years, 1 month ago) by nogin
File length: 5785 byte(s)
Diff to previous 2661
I hope I've fixed the OSTYPE/pthreads check.


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: 5764 byte(s)
Diff to previous 2658
- 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 2658 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 20 21:27:59 1999 UTC (22 years, 1 month ago) by nogin
File length: 5740 byte(s)
Diff to previous 2637
Added the Refiner information (VERBOSE/SIMPLE and ds/std) into mp_version


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: 5615 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: 5600 byte(s)
Diff to previous 2582
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 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: 5580 byte(s)
Diff to previous 2574
- 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 2574 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 25 18:34:13 1999 UTC (22 years, 4 months ago) by jyh
File length: 5581 byte(s)
Diff to previous 2573
Added edit_set_goal, which loads the package if it is not yet loaded.


Revision 2573 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 25 18:21:31 1999 UTC (22 years, 4 months ago) by jyh
File length: 5583 byte(s)
Diff to previous 2566
Distributed refiner for CADE-16.


Revision 2566 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 12 22:36:39 1999 UTC (22 years, 5 months ago) by nogin
File length: 6223 byte(s)
Diff to previous 2564
Set LC_ALL and LANG environment variables to "C" when creating
mp_version.ml, so that the date in mp_version would always be in English


Revision 2564 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 8 21:51:02 1999 UTC (22 years, 5 months ago) by jyh
File length: 6191 byte(s)
Diff to previous 2552
This is the version of the distributed prover used in the
CADE-16 original paper.  I'm still adjusting it though, so
that we can use term_ds and native-code.

If any of you have problems compiling clib/mmap.c, let me know.  It
should compile on Linux and Win32, but we should put in stubs
if there are problems on other systems.


Revision 2552 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 2 22:23:32 1999 UTC (22 years, 5 months ago) by nogin
File length: 6220 byte(s)
Diff to previous 2550
Fixed the build with undefined OCAMLSRC and the native code build


Revision 2550 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 2 16:47:14 1999 UTC (22 years, 5 months ago) by jyh
File length: 6191 byte(s)
Diff to previous 2549
Fixed some problems with Ensemble.
The closure marshaler was marshaling huge closures containing
Ensemble itself. I think I have fixed this problem.
The performance numbers may change slightly due to a
modification of thread_refiner_null, which now composes
extracts only after an entire proof is done.


Revision 2549 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 1 20:14:13 1999 UTC (22 years, 5 months ago) by jyh
File length: 6261 byte(s)
Diff to previous 2529
Fixed up "make clean" to remove more files.
The directory should be like a new checkout afterwards.
Enabled set_debug function in toploop.  You can
turn on debugging with

# set_debug "xxx" true;;

for some debug variable xxx.


Revision 2529 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 29 23:30:21 1998 UTC (22 years, 5 months ago) by jyh
File length: 6247 byte(s)
Diff to previous 2512
Added pigeonhole problem in editor/ml/test.ml.

To try it:

% ./mptop
# #use "y.ml";;
# refine timingT proveT;;


Revision 2512 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 21:31:37 1998 UTC (22 years, 8 months ago) by nogin
File length: 6240 byte(s)
Diff to previous 2502
For removing files, always use $(RM)
RM is currently defined in mk/config to be "rm -f"


Revision 2502 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 09:01:06 1998 UTC (22 years, 8 months ago) by nogin
File length: 6240 byte(s)
Diff to previous 2497
More NL -> MP changes


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: 6243 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: 6243 byte(s)
Diff to previous 2493
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 2493 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 12 22:40:01 1998 UTC (22 years, 8 months ago) by jyh
File length: 6261 byte(s)
Diff to previous 2487
Added "reflection" theory, for reflecting sentences in the meta-logic
into the Nuprl type theory.


Revision 2487 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 5 17:42:34 1998 UTC (22 years, 8 months ago) by lolorigo
File length: 6085 byte(s)
Diff to previous 2484
Added library_eval (moved from ../../library because of
dependency on nl functions).
Modified library_eval and added library_test to support
interaction with Nuprl 5 interface.


Revision 2484 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 30 22:23:03 1998 UTC (22 years, 8 months ago) by nogin
File length: 5952 byte(s)
Diff to previous 2483
Make Eli's nl_version hack work correctly (I hope)
on both native and bytecode builds


Revision 2483 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 30 22:17:16 1998 UTC (22 years, 8 months ago) by eli
File length: 5633 byte(s)
Diff to previous 2481
Fixed stupid stuff.


Revision 2481 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 30 00:51:50 1998 UTC (22 years, 8 months ago) by eli
File length: 5525 byte(s)
Diff to previous 2473
Made nl_version.ml depend on everything but itself and the executables, so
repeating make does nothing new.
At least I hope I did that - can you makefile-wizards check what I did?


Revision 2473 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 23 20:34:33 1998 UTC (22 years, 9 months ago) by jyh
File length: 5542 byte(s)
Diff to previous 2466
Fixed loading in edit_list_module.


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: 5422 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: 5367 byte(s)
Diff to previous 2455
More CAMLP4LIB changes


Revision 2455 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 21:02:22 1998 UTC (22 years, 9 months ago) by jyh
File length: 5350 byte(s)
Diff to previous 2452
Added version numbering.


Revision 2452 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 27 13:45:19 1998 UTC (22 years, 9 months ago) by jyh
File length: 5151 byte(s)
Diff to previous 2443
Fixed the thread problem without Ensemble.  Removed the library
temporarily until files can be upgraded to OCaml 2.0.


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: 5257 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: 5348 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: 3499 byte(s)
Diff to previous 2407
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 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: 3521 byte(s)
Diff to previous 2404
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 2404 - (view) (download) (annotate) - [select for diffs]
Modified Tue Aug 4 23:46:32 1998 UTC (22 years, 10 months ago) by jyh
File length: 3511 byte(s)
Diff to previous 2387
Fixed a problem with Fun_splay_set.union, which was introducing
non-sorted splay trees.


Revision 2387 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 2 20:58:11 1998 UTC (22 years, 10 months ago) by nogin
File length: 3511 byte(s)
Diff to previous 2376
Pass all $(OCAMLOPTFLAGS) to ocamlopt when building nl.opt


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: 3505 byte(s)
Diff to previous 2336
Added TPTP theory, and Ensemble library.  Fixed sequent displays.
BUG: rewrites fail on sequents.


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: 3372 byte(s)
Diff to previous 2325
Added NL toploop so that we can compile NL native code.


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


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: 1849 byte(s)
Diff to previous 2258
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 2258 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 17 15:46:02 1998 UTC (23 years ago) by jyh
File length: 1852 byte(s)
Diff to previous 2244
Optimizing compiler.


Revision 2244 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 15 22:33:52 1998 UTC (23 years ago) by jyh
File length: 1899 byte(s)
Diff to previous 2224
Added CZF.


Revision 2224 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 12 13:47:49 1998 UTC (23 years ago) by jyh
File length: 1818 byte(s)
Diff to previous 2222
D tactic works, added itt_bool.


Revision 2222 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 9 20:53:04 1998 UTC (23 years ago) by jyh
File length: 1808 byte(s)
Diff to previous 2209
Propagated refinement changes.
New tacticals module.


Revision 2209 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 13:57:13 1998 UTC (23 years ago) by jyh
File length: 1782 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: 1795 byte(s)
Diff to previous 2190
Better Makefiles.


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


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: 1657 byte(s)
Diff to previous 2160
The right paths to prlc, ocamldep, etc in Makefiles


Revision 2160 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 29 20:54:17 1998 UTC (23 years, 1 month ago) by jyh
File length: 1643 byte(s)
Diff to previous 2159
Initial working display forms.


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: 1636 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: 1539 byte(s)
Diff to previous 2153
ls() works, adding display.


Revision 2153 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 24 19:39:13 1998 UTC (23 years, 2 months ago) by jyh
File length: 1585 byte(s)
Diff to previous 2152
Updated debugging.


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: 1524 byte(s)
Diff to previous 2151
Added more extensive debugging capabilities.


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: 1519 byte(s)
Diff to previous 2143
Initial rebuilt editor.


Revision 2143 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 20:48:40 1998 UTC (23 years, 2 months ago) by jyh
File length: 587 byte(s)
Diff to previous 2137
Updating refiner for extraction.


Revision 2137 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 17 01:31:36 1998 UTC (23 years, 2 months ago) by jyh
File length: 561 byte(s)
Diff to previous 2129
Editor is almost constructed.


Revision 2129 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 15 22:29:02 1998 UTC (23 years, 2 months ago) by jyh
File length: 605 byte(s)
Diff to previous 2122
Converting packages from summaries.


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


Revision 2119 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 9 19:07:29 1998 UTC (23 years, 2 months ago) by jyh
File length: 591 byte(s)
Diff to previous 2107
Updating the editor.


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: 554 byte(s)
Diff to previous 2050
ImpDag is in mllib.


Revision 2050 - (view) (download) (annotate) - [select for diffs]
Added Wed Aug 6 16:25:52 1997 UTC (23 years, 10 months ago) by jyh
File length: 1072 byte(s)
Makefile for editor.


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