/[mojave]/metaprl/Makefile
ViewVC logotype

Log of /metaprl/Makefile

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

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: 4366 byte(s)
Diff to previous 3582
- 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 3582 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 24 23:51:09 2002 UTC (19 years, 2 months ago) by nogin
File length: 4413 byte(s)
Diff to previous 3450
Added "make latex" target.


Revision 3450 - (view) (download) (annotate) - [select for diffs]
Modified Mon Nov 19 20:39:56 2001 UTC (19 years, 7 months ago) by nogin
File length: 4299 byte(s)
Diff to previous 3429
Added some additional info to comments in JProver files.


Revision 3429 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 28 22:06:32 2001 UTC (19 years, 7 months ago) by nogin
File length: 4227 byte(s)
Diff to previous 3419
- Made sure that div by zero and mod zero raise proper exceptions in
Mp_big_int, Mp_num and Base_meta
- Made the Mp_num.num and Mp_big_int.big_int types abstract.
- Minor changes in the "make realclean" scripts.


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: 4186 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: 4296 byte(s)
Diff to previous 3073
- 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 3073 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 23 20:50:23 2000 UTC (20 years, 9 months ago) by nogin
File length: 4268 byte(s)
Diff to previous 3063
Some of the functions were not wrapped in print_exn for some reason - fixed.


Revision 3063 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 19 05:09:30 2000 UTC (20 years, 9 months ago) by nogin
File length: 4275 byte(s)
Diff to previous 3029
1) "define" currently can't handle recursive difinitions.
The proper way of doing them is through Y-combinator (a-la-Nuprl),
but for defining factorial in itt_test, a declare+prim_rw is good enough.

2) Traded "nasty" make warnings for a little less nastier ones.


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


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: 4224 byte(s)
Diff to previous 2858
- 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 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: 4207 byte(s)
Diff to previous 2842
Added a check that makes sure that a correct version of Ocaml and Camlp4
is used.


Revision 2842 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 3 02:21:17 1999 UTC (21 years, 7 months ago) by nogin
File length: 4218 byte(s)
Diff to previous 2826
Added "make realclean" target that uses CVS information and interactively removes
all the files that have no CVS entries associated with them.


Revision 2826 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 26 20:47:53 1999 UTC (21 years, 8 months ago) by nogin
File length: 4184 byte(s)
Diff to previous 2825
- Added documentation on how to convert documentation .PS and .PDF formats.

- Removed mp-frame.html - as far as I can see, it is just an outdated
version of mp.html

- Added more HTML files to system.{ps,pdf}


Revision 2825 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 26 02:44:44 1999 UTC (21 years, 8 months ago) by nogin
File length: 4098 byte(s)
Diff to previous 2793
- Added a Makefile target "check" that checks HTML syntax
using weblint utility ( http://www.weblint.org/ )

- Fixed most of the HTML problems reported by weblint utility
This reduced the number of weblint warnings from over 8000 to 19
(All 19 are
   unknown attribute "..." for element <FRAMESET>
where ... is either FRAMEBORDER, BORDER or FRAMESPACING)

- Added system.{ps,pdf} (MetaPRL System Description)
to the list of generated documentation files

- Some htmldoc-related fixes

- Removed the references to "load" command since
in the current version of MetaPRL "cd" command loads
the module if necessary.

- Removed some unused test files


Revision 2793 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 7 16:24:35 1999 UTC (21 years, 11 months ago) by nogin
File length: 4094 byte(s)
Diff to previous 2777
Do not keep normalazing the same opnames over and over.

Added filter_opt target, useful to get convert, etc compiled into the native code


Revision 2777 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 19:35:12 1999 UTC (21 years, 11 months ago) by nogin
File length: 3947 byte(s)
Diff to previous 2775
Handle THEORIES variable a little better


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: 3908 byte(s)
Diff to previous 2753
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 2753 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 25 00:19:15 1999 UTC (22 years ago) by jyh
File length: 4008 byte(s)
Diff to previous 2747
These are some minor changes to make things work better.  Changed
meaning of ThinOption in elim_resource: it now means to thin the hyp
by default, unless overridden by thinningT false.

Fixed some proof operations.  Added "move_to_assum" command to take
the current subgoal and make it an extra assumption of the entire
proof (it may not work at the moment).

ls now takes a _string_ argument.  Use ls "u";; to display only the
unproved rules in the current module.

Proved many membership variants of the standard type constructors,
but there are a few more to go.  When you are defining theories, I
believe you should use membership, not equality.  After all, equality
is derivable from membership, and membership is a lot easier.

Still to go: ASCII format proof files; save proofs _without_ extracts
by default.  The expand () function does not reexpand proofs correctly.
A few problems with proof navigation.


Revision 2747 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 23:40:57 1999 UTC (22 years ago) by nogin
File length: 4003 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: 3944 byte(s)
Diff to previous 2706
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 2706 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 13 02:34:07 1999 UTC (22 years ago) by nogin
File length: 3943 byte(s)
Diff to previous 2637
Small changes


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: 3928 byte(s)
Diff to previous 2621
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 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: 3886 byte(s)
Diff to previous 2613
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=
   solaris

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


Revision 2613 - (view) (download) (annotate) - [select for diffs]
Modified Wed Mar 10 04:15:48 1999 UTC (22 years, 3 months ago) by nogin
File length: 3794 byte(s)
Diff to previous 2599
"make depend" should just go and erase all Makefile.dep files since
subsequent make would rebuild them


Revision 2599 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 24 02:08:29 1999 UTC (22 years, 4 months ago) by nogin
File length: 3780 byte(s)
Diff to previous 2590
Added profile_mem goal that allows one to profile memory allocation


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: 3241 byte(s)
Diff to previous 2584
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 2584 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 2 02:24:12 1999 UTC (22 years, 4 months ago) by nogin
File length: 3027 byte(s)
Diff to previous 2583
Fixed the native code profiling build - added back the filter goal


Revision 2583 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 2 02:05:03 1999 UTC (22 years, 4 months ago) by nogin
File length: 2866 byte(s)
Diff to previous 2582
Jason says we do not need -g gcc option anymore
Also, I've decided it's better if make clean checks config file too


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: 2853 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: 2691 byte(s)
Diff to previous 2550
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 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: 2321 byte(s)
Diff to previous 2535
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 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: 2313 byte(s)
Diff to previous 2514
Fixed the bytecode profiling build.

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


Revision 2514 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 21:54:52 1998 UTC (22 years, 8 months ago) by nogin
File length: 2265 byte(s)
Diff to previous 2513
Use "make -C $$i" instead of "cd $$i; make" to avoid problems in case directory
does not exist.


Revision 2513 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 21:37:53 1998 UTC (22 years, 8 months ago) by nogin
File length: 2273 byte(s)
Diff to previous 2497
Start "make clean" by cleaning lib and bin


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: 2271 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: 2271 byte(s)
Diff to previous 2490
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 2490 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 6 14:08:25 1998 UTC (22 years, 8 months ago) by jyh
File length: 2248 byte(s)
Diff to previous 2477
Added evaluation functions to ShellP4.
Lori: the "open" functions do not work in edit_cd_thm.  I believe
that the "open" expresssions are evaluated in a separate toploop,
so there is no way to open the module in the real toploop
except by typing it in...


Revision 2477 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 29 00:33:29 1998 UTC (22 years, 8 months ago) by jyh
File length: 2238 byte(s)
Diff to previous 2466
Added some features Lori requested for the Nuprl5 editor, plus
a syntax fix in the Fol_implies 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: 2223 byte(s)
Diff to previous 2452
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 2452 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 27 13:45:19 1998 UTC (22 years, 10 months ago) by jyh
File length: 2077 byte(s)
Diff to previous 2442
Fixed the thread problem without Ensemble.  Removed the library
temporarily until files can be upgraded to OCaml 2.0.


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: 2087 byte(s)
Diff to previous 2398
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 2398 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 3 12:55:18 1998 UTC (22 years, 10 months ago) by nogin
File length: 2076 byte(s)
Diff to previous 2386
Fixed profiling build


Revision 2386 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 2 20:48:09 1998 UTC (22 years, 10 months ago) by nogin
File length: 2054 byte(s)
Diff to previous 2376
Added editor/ml directory to the profiled build


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


Revision 2373 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 30 13:43:16 1998 UTC (22 years, 10 months ago) by nogin
File length: 1900 byte(s)
Diff to previous 2363
Added optimized code profiled compilation (make profile)


Revision 2363 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jul 25 07:03:48 1998 UTC (22 years, 11 months ago) by nogin
File length: 1603 byte(s)
Diff to previous 2336
No need to make opt twice in editor/ml


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


Revision 2270 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 22 21:41:47 1998 UTC (23 years ago) by nogin
File length: 1632 byte(s)
Diff to previous 2268
Better profiling


Revision 2268 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 22 19:46:48 1998 UTC (23 years ago) by jyh
File length: 1591 byte(s)
Diff to previous 2265
Rewriting in contexts.  This required a change in addressing,
and the body of the context is the _last_ subterm, not the first.


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


Revision 2251 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 16 16:26:27 1998 UTC (23 years ago) by jyh
File length: 1457 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: 1341 byte(s)
Diff to previous 2244
"make profile" seems to be working


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


Revision 2210 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 1 19:29:16 1998 UTC (23 years ago) by jyh
File length: 1025 byte(s)
Diff to previous 2201
*** empty log message ***


Revision 2201 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 29 14:53:34 1998 UTC (23 years ago) by jyh
File length: 1010 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: 1313 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: 1187 byte(s)
Diff to previous 2164
The right paths to prlc, ocamldep, etc in Makefiles


Revision 2164 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 1 18:43:42 1998 UTC (23 years, 1 month ago) by jyh
File length: 1154 byte(s)
Diff to previous 2093
Added raw display.


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


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: 859 byte(s)
Diff to previous 2051
This version compiles Ensemble.


Revision 2051 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 6 16:33:12 1997 UTC (23 years, 10 months ago) by jyh
File length: 849 byte(s)
Diff to previous 2049
Minor changes.


Revision 2049 - (view) (download) (annotate) - [select for diffs]
Added Wed Aug 6 16:24:08 1997 UTC (23 years, 10 months ago) by jyh
File length: 841 byte(s)
System Makefile.


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