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

Log of /metaprl/editor/ml/OMakefile

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 9643 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 28 17:47:14 2006 UTC (14 years, 7 months ago) by nogin
File length: 6300 byte(s)
Diff to previous 9332
Made MetaPRL compile with the latest 0.9.8 OMake.


Revision 9332 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 16 18:01:48 2006 UTC (15 years ago) by jyh
File length: 6306 byte(s)
Diff to previous 8594
Use @echo instead of println in .PHONY/editor/ml/done.


Revision 8594 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 21:33:35 2006 UTC (15 years, 4 months ago) by nogin
File length: 6309 byte(s)
Diff to previous 8593
Making "omake clean" more clean.


Revision 8593 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 21:28:28 2006 UTC (15 years, 4 months ago) by nogin
File length: 6300 byte(s)
Diff to previous 8585
- Making the "omake clean" more clean, while making sure that in shared mode,
  "omake clean" would not try cleaning up the shared installation.

- Removing the "bin" and "lib" directories - they should now be created
  on-demand.


Revision 8585 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 04:51:23 2006 UTC (15 years, 4 months ago) by nogin
File length: 6267 byte(s)
Diff to previous 8584
- When no port is given (or when -port 0 is given), use the first free port
  starting with the default 60,000.

- If the HTTP server failed to start up (the port is in use, etc), print a
  better error message.


Revision 8584 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 04:35:59 2006 UTC (15 years, 4 months ago) by jyh
File length: 6257 byte(s)
Diff to previous 8566
Include .test-metaprl-startup on "omake install".

Added code to check reduce annotations for progress.
Amazingly, the only rewrite that does not pass the test
is Itt_hoas_relax.squash_bdepth_mk_terms.  Perhaps my
test is too relaxed.


Revision 8566 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jan 22 06:52:22 2006 UTC (15 years, 5 months ago) by nogin
File length: 6175 byte(s)
Diff to previous 8555
The new symlinks should be ignored by SVN and deleted by "omake clean".


Revision 8555 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jan 22 00:37:23 2006 UTC (15 years, 5 months ago) by nogin
File length: 6166 byte(s)
Diff to previous 8547
Keep all the scripts in support/editor. All the scripts that are postentially
applicable will be installed and linked into editor/ml. Irrelevant scripts
(such as mprun when MPRUN_ENABLED is false and mpgossip when ENSROOT is
undefined) will be ignored.


Revision 8547 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 21 16:18:01 2006 UTC (15 years, 5 months ago) by jyh
File length: 6178 byte(s)
Diff to previous 8546
Temporarily, at least, link the mpopt script into editor/ml
so the tests work.


Revision 8546 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 21 15:45:47 2006 UTC (15 years, 5 months ago) by jyh
File length: 6086 byte(s)
Diff to previous 8539
Move the MetaPRL scripts from editor/ml into support/editor
so that readonly clients do not need to copy them.


Revision 8539 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 21:38:29 2006 UTC (15 years, 5 months ago) by nogin
File length: 6079 byte(s)
Diff to previous 8534
Fixed bytecode compilation (including mp.run)

Revision 8534 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 06:31:53 2006 UTC (15 years, 5 months ago) by jyh
File length: 6064 byte(s)
Diff to previous 8528
Yay!  The standalone MetaPRL brings up the browser.


Revision 8528 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 04:36:11 2006 UTC (15 years, 5 months ago) by jyh
File length: 6063 byte(s)
Diff to previous 8519
Added the INSTALL_DIR option to mk/config, and generate
the OMakeroot_install and editor/ml/mpconfig files.

Next up: add the search path for theories.


Revision 8519 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 01:39:06 2006 UTC (15 years, 5 months ago) by nogin
File length: 5257 byte(s)
Diff to previous 8518
Cleaning up things after Jason's big "shared r/o installation" commit,
including:

- Cleaning up the dups between the editor/ml and support/editor.

- Moved all the compiled test files (as opposed to test files that are
  indended to be used on the MetaPRL command line) from editor/ml/tests to
  theories/itt/tests

- Updated all the places that still pointed to editor/ml/svnversion.txt to use
  to support/editor/svnversion.txt or $(LIB)/svnversion.txt as appropriate.

- Added a LibInstall function for installing things into the $(LIB) directory
  and LibSubInstall for installing things into subdirectories of the $(LIB)
  directory.


Revision 8518 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 19 22:03:05 2006 UTC (15 years, 5 months ago) by jyh
File length: 5835 byte(s)
Diff to previous 8510
Reconfigure MetaPRL to allow an installable version.
Mostly finished, but see the notes below.

To do it:
   - Run "omake install"
     This installs a binary version of MetaPRL into
     <installdir>, which is currently metaprl/export.

   - In your private directory,
     1. Link/copy <installdir>/mk/OMakeroot
     2. Copy mpconfig
     3. Create an OMakefile with a line
        THEORIES = <names>
     Now you can run omake and it will produce an
     executable called "mp".

NOTES:
   - It is uglier than it should be, mainly because of
     special-casing for theories/meta/base.  This should
     be discussed, find a better solution.
     
   - The location of the <installdir> should be configurable
     in mk/config.

   - The initial private user setup should be scripted.


Revision 8510 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 19 04:14:00 2006 UTC (15 years, 5 months ago) by jyh
File length: 7378 byte(s)
Diff to previous 8410
Prepare an installable version of MetaPRL.
The following directories are collected into libraries,
and copied into a standard install location.

   libmojave
   mllib
   refiner
   filter
   support
   editor/ml

For each of these directories, the .mli,.cmi and the
library itself are copied to an <install>/lib directory.
In addition, the filter directory copies the camlp4{n,o}
executables.

Note that the other filter/ binaries are currently broken.
We'll need to fix someday.

The plan is:

   1. Install these files into a standard location like
      /usr/lib/metaprl.  TODO: add the location of the
      install directory to mk/config.

   2. Build a new OMakeroot that will allow people
      to build their own private copy of MetaPRL
      with their own theories, just from these
      binaries.

   3. (Probably) build a binary MetaPRL RPM.

Note: the current install target is called "export", because
we have a pre-existing "install" target.  I don't know what
the "install" was used for, but it seems like we should
usurp it for the current purpose.

I'll finish #2 tomorrow.


Revision 8410 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 6 06:42:29 2006 UTC (15 years, 5 months ago) by nogin
File length: 7149 byte(s)
Diff to previous 8401
(Issue 561) The format of editor/ml/mldebug.dir is different on Windows.


Revision 8401 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 5 21:16:41 2006 UTC (15 years, 5 months ago) by nogin
File length: 7050 byte(s)
Diff to previous 8149
Include the SVN revision number (when available) in the MetaPRL version string.


Revision 8149 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 9 08:19:55 2005 UTC (15 years, 7 months ago) by nogin
File length: 6357 byte(s)
Diff to previous 8127
- Made sure that documentation generator plays nicely with the new THEORY_DEPS
  mechanism.

- Further clean-ups in the THEORY_DEPS implementation.


Revision 8127 - (view) (download) (annotate) - [select for diffs]
Modified Tue Nov 8 03:11:12 2005 UTC (15 years, 7 months ago) by nogin
File length: 6452 byte(s)
Diff to previous 8025
(Issue 543) Compute the full list of theories to build based on the
inter-theory dependencies.

Now that ITT is composed of a bunch of smaller subtheories, having to specify
the full list of theories in mk/config became more annoying. This commit
implements the notion of theory dependencies and uses it to compute the full
list of theories to be compiled. Now setting THEORIES in mk/config to
something like "poplmark/naive" should work, bringing in all the necessary
dependencies.

In order to work correctly, the theory/*/OMakefile:

- MAY define or update the THEORY_DEPENCIES variable. This variable MUST
  contain an array of theory "names" (as before, the theory "name" is the
  directory name relative to $(ROOT)/theories). By default, THEORY_DEPENCIES
  is equal to "base"

- SHOULD use either the Theory function (which takes a file list as an
  argument), or a VirtualTheory function (this takes a list of subdirectories
  as an argument and should be used for "virtual" theories that only bring
  together sub-theories, but do not contain any modules). Note that
  VirtualTheory overrides the THEORY_DEPENCIES variable, so any additonal
  modifications to THEORY_DEPENCIES in virtual theories (which usually
  shouldn't be necessary) need to go after the VirtualTheory call.

- SHOULD NOT change the OCAMLINCLUDES variable (except for non-theory
  directories). The standard "Theory" function now sets OCAMLINCLUDES based on
  the value of THEORY_DEPENCIES, and if the resulting value is incorrect, it
  is usually a very good indication that THEORY_DEPENCIES is also incorrect.

- SHOULD NOT use .SUBDIRS to bring in other theories; it should use
  THEORY_DEPENCIES or VirtualTheory mechanism instead.


Revision 8025 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 28 10:39:44 2005 UTC (15 years, 7 months ago) by nogin
File length: 6416 byte(s)
Diff to previous 8024
Create a symlink editor/ml/mp -> editor/ml/mpopt (or top) so there is always a
"canonical" way of starting MetaPRL, regardless of the compilation mode. On
Windows, copy the appropriate .bat into editor/ml/mp.bat


Revision 8024 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 28 10:25:33 2005 UTC (15 years, 7 months ago) by nogin
File length: 6451 byte(s)
Diff to previous 7968
- Issue 538: At the end of the build process, delete any outdated binaries in
  editor/ml.

- Issue 539: Added an MPRUN_ENABLED variable that controls whether to build
  the mp.run binary (defaults to false)

- Renamed the old editor/ml/mp script into editor/ml/mprun (for consistency).

- Updated the mpopt/mptop scripts to give a better error message when the
  corresponding binary does not exist.


Revision 7968 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 22 04:32:26 2005 UTC (15 years, 8 months ago) by nogin
File length: 6166 byte(s)
Diff to previous 7964
Bug 534: use "echo > $@" instead of touch "$@" for portability

Revision 7964 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 22 01:28:47 2005 UTC (15 years, 8 months ago) by nogin
File length: 6165 byte(s)
Diff to previous 7956
Adding PHONY targets for running MetaPRL once it compiles.

Revision 7956 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 21 03:09:16 2005 UTC (15 years, 8 months ago) by nogin
File length: 6001 byte(s)
Diff to previous 7955
Added a "mixed" compilation mode that builds a native code filter and a
bytecode toploops. This may be the optimal mode when doing a lot of theory
development, but the proofs are fairly simple, so I made it the default mode.

The config file now has a single "COMPILATION_MODE" variable (possible values:
byte, native, both and mixed) instead of NATIVE_ENABLED/BYTE_ENABLED.

Warning: if you want something other than the default "mixed", make sure to
edit your mk/config after "svn up; omake mk/config".


Revision 7955 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 21 02:55:39 2005 UTC (15 years, 8 months ago) by nogin
File length: 5731 byte(s)
Diff to previous 7952
THe theories/itt/core include is only needed by the editor/ml/tests directory
(where it is not so unreasonable to have it hardcoded).


Revision 7952 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 21 02:36:52 2005 UTC (15 years, 8 months ago) by jyh
File length: 5811 byte(s)
Diff to previous 7674
Various fixes to get things to compile again.
Note the hardcoded theories/itt/core in editor/ml/OMakefile.
This should be fixed.


Revision 7674 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 5 17:50:59 2005 UTC (15 years, 10 months ago) by jyh
File length: 5731 byte(s)
Diff to previous 7538
Minimal changes for compatibility with omake 0.9.7.


Revision 7538 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jul 2 14:02:24 2005 UTC (15 years, 11 months ago) by jyh
File length: 5691 byte(s)
Diff to previous 7321
Update to match the recent changes to omake.


Revision 7321 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 23 20:05:36 2005 UTC (16 years, 1 month ago) by jyh
File length: 5690 byte(s)
Diff to previous 7316
Removed the DIRSEP.  But I can't figure out where this variable
was defined...  Maybe Yegor had it defined in his environment?


Revision 7316 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 23 04:45:36 2005 UTC (16 years, 1 month ago) by nogin
File length: 5698 byte(s)
Diff to previous 7315
Follow-up to Yegor's change: just use the DIRSEP variable.


Revision 7315 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 23 04:17:00 2005 UTC (16 years, 1 month ago) by yegor
File length: 5787 byte(s)
Diff to previous 7273
I had this on win32:
------
build editor\ml .test-metaprl-startup
+ echo | ./mpopt.bat -batch
'.' is not recognized as an internal or external command,
operable program or batch file.
*** omake: 4086/4185 targets are up to date
*** omake: failed (12.8 sec, 0/888 scans, 1/1982 rules, 1/5523 digests)
*** omake: targets were not rebuilt because of errors:
   editor\ml\.test-metaprl-startup
      depends on: editor\ml\mpconfig
      depends on: editor\ml\mpopt.bat
--------

Apprently it does not like "./", so I use ".\" for win32


Revision 7273 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 13 01:09:07 2005 UTC (16 years, 1 month ago) by jyh
File length: 5683 byte(s)
Diff to previous 7269
Removed some Win32-specific variables that are no longer needed.


Revision 7269 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 12 23:10:29 2005 UTC (16 years, 1 month ago) by jyh
File length: 5700 byte(s)
Diff to previous 7268
This is an update to match the recent changes to omake.  This is
mainly a change to use explicit :scanner: dependencies.

The omake log message was as follows.

------------------------------------------------------------------------

This is a significant change to .SCANNER rules, where .SCANNER rules
are treated much more like normal rules.

Externally, a .SCANNER rule has the usual rule form:

   .SCANNER: target: dependencies...
      ...scanner commands...

In this commit, the scanner target is now decoupled from the
build target, allowing a scanner result to be used for multiple
build targets.  For example, ocamldep produces dependencies
for .cmo and .cmx files simultaneously.  They can share
the scanner rule by specifying an explicit :scanner: dependency.

    .SCANNER: scan-ocaml-%.ml: %.ml
        ocamldep $<

    %.cmo: %.ml :scanner: scan-ocaml-%.ml
        $(OCAMLC) ...

    %.cmx %.o: %.ml :scanner: scan-ocaml-%.ml
        $(OCAMLOPT) ...

The current convention is that scanner targets should be named
scan-<language>-<source-file>.

   -- If a rule has multiple :scanner: dependencies, the actual
      dependencies will be the union of the scanner results.

   -- The .SCANNER targets use a different namespace than
      normal targets, so it is valid to have overlapping rules.

          .SCANNER: foo:
              echo "foo: boo"

          foo: :scanner: foo
              ...

   -- For backwards compatibility, if a rule has no :scanner:
      dependencies, then omake will try to find a scanner with
      the same name as the target.  So in the example above,
      the :scanner: foo is actually unnecessary.


Revision 7268 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 12 22:35:19 2005 UTC (16 years, 1 month ago) by nogin
File length: 5723 byte(s)
Diff to previous 7262
Fixed a build issue caused by an empty [OPT]THREADSLIB variable in an array,
when threads are disabled.


Revision 7262 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 12 06:25:18 2005 UTC (16 years, 1 month ago) by nogin
File length: 5753 byte(s)
Diff to previous 7237
A "uniformity" pass over the OMakefiles:

- Turned the file lists into arrays (except when bug 475 makes it hard)

- Turned "tab" symbols into spaces

- Inlined the "Files" files that were only included once.


Revision 7237 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 30 23:52:35 2005 UTC (16 years, 1 month ago) by jyh
File length: 6124 byte(s)
Diff to previous 6937
Working on outstanding issues for Win32.

This is a fix to be more careful about spaces in filenames,
so that placing ocaml in

   C:\Program Files\Objective Caml

actually works.  This adds the $(quote-argv ...) function that
quotes an array in a way that the command-line parser can recover
the argv string.  This allows include directories with spaces in
a -pp option.


Revision 6937 - (view) (download) (annotate) - [select for diffs]
Modified Wed Mar 16 00:28:20 2005 UTC (16 years, 3 months ago) by nogin
File length: 6107 byte(s)
Diff to previous 6575
Proper scoping for OCamlGeneratedFiles.


Revision 6575 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 3 08:41:07 2005 UTC (16 years, 4 months ago) by nogin
File length: 6102 byte(s)
Diff to previous 6468
Do not include the tests directory, unless any test files are actually in use.


Revision 6468 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 22 02:08:31 2005 UTC (16 years, 5 months ago) by nogin
File length: 6080 byte(s)
Diff to previous 6445
Reduced the number of things that are compiled with -linkall.

Now compiled w/o -linkall:
- most helper libraries (including libmojave)
- MetaPRL main binary (3.5% reduction in size of mp.opt)

Still compiled with -linkall:
- All the theory libraries (because their contents are the whole point!)
- The filter binaries - this is pretty unfortunate, but the way camlp4 is
  compiled makes this almost unavoidable. I've filed
    http://caml.inria.fr/bin/caml-bugs?selectid=3439 about this.


Revision 6445 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 19 22:40:52 2005 UTC (16 years, 5 months ago) by nogin
File length: 6137 byte(s)
Diff to previous 6403
Make it easier to mix MetaPRL and non-MetaPRL .ml files in theories.

This is useful because non-MetaPRL compilation makes .mli optional,
is faster, iand can be done without waiting for the filter to be built.


Revision 6403 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 14 09:49:38 2005 UTC (16 years, 5 months ago) by nogin
File length: 6096 byte(s)
Diff to previous 6401
Bug 386 workaround for the "test-metaprl-startup" target


Revision 6401 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 14 04:02:25 2005 UTC (16 years, 5 months ago) by nogin
File length: 6084 byte(s)
Diff to previous 6388
Some fixes in the "omake check-status" rules


Revision 6388 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 11 05:42:14 2005 UTC (16 years, 5 months ago) by nogin
File length: 6076 byte(s)
Diff to previous 6373
The .DEFAULT target now includes a "test-metaprl-startup" target which
checks whether MetaPRL can start up successfully. This means that if somebody
introduces a bug that is only visible at runtime, then a simple "omake"
will detect it (making it less likely that the bug will be accidentally
checked in).


Revision 6373 - (view) (download) (annotate) - [select for diffs]
Modified Fri Dec 31 05:17:20 2004 UTC (16 years, 5 months ago) by nogin
File length: 5785 byte(s)
Diff to previous 6367
Avoid having to symlink/copy libs into the lib directory just to compile
MetaPRL.


Revision 6367 - (view) (download) (annotate) - [select for diffs]
Modified Wed Dec 29 05:58:46 2004 UTC (16 years, 5 months ago) by nogin
File length: 5594 byte(s)
Diff to previous 6336
Fixed some of the issues with duplicated and/or absolute paths in
OCAMLINCLUDES. Should fix (or rather work around) bug 372, could also fix bug
373.


Revision 6336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 7 02:09:15 2004 UTC (16 years, 6 months ago) by nogin
File length: 5587 byte(s)
Diff to previous 6242
(bug 181) Auto-generate the list of the include directories.


Revision 6242 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 15 23:28:44 2004 UTC (16 years, 8 months ago) by nogin
File length: 5582 byte(s)
Diff to previous 6241
Fixing a typo in my previous commit.


Revision 6241 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 15 23:22:40 2004 UTC (16 years, 8 months ago) by nogin
File length: 5580 byte(s)
Diff to previous 6148
The tests that require ITT should not be compiled unless ITT is listed in
the THEORIES variable.


Revision 6148 - (view) (download) (annotate) - [select for diffs]
Modified Mon Aug 30 02:09:44 2004 UTC (16 years, 9 months ago) by jyh
File length: 5512 byte(s)
Diff to previous 6124
Merged the shell_begin branch.


Revision 6124 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 20 05:41:44 2004 UTC (16 years, 10 months ago) by nogin
File length: 5519 byte(s)
Diff to previous 6109
MP_DIRS needs to be an array in the first place; fixing it later with a split
is a bad idea since this causes the effects of $(dir ...) to be lost (which
was why the editor/ml/tests directory could not be compiled).


Revision 6109 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 28 21:21:53 2004 UTC (16 years, 10 months ago) by crt
File length: 5535 byte(s)
Diff to previous 6107
Fixed the MP_DIRS problem.
Added a split call on MP_DIRS where the array OCAMLINCLUDES
was created (editor/ml/OMakefile)

OCAMLINCLUDES[] +=
        $(ROOT)/$(ENSEMBLE_DIR)
        $(split ' ',$(MP_DIRS))


Revision 6107 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 26 20:04:22 2004 UTC (16 years, 10 months ago) by jyh
File length: 5528 byte(s)
Diff to previous 6086
Removed all -I suffixes from INCLUDES


Revision 6086 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 15 02:07:52 2004 UTC (16 years, 11 months ago) by nogin
File length: 5550 byte(s)
Diff to previous 5974
Added dependencies on camlp4 (actually - camlp4o and camlp4r) and
ocamlmktop versions. This should complete the bug 47 requirements.


Revision 5974 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 09:21:16 2004 UTC (17 years ago) by nogin
File length: 5528 byte(s)
Diff to previous 5910
mp.opt depends on the .o files, not just the .cmx ones.


Revision 5910 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 16 22:59:05 2004 UTC (17 years ago) by nogin
File length: 5466 byte(s)
Diff to previous 5847
- Include -lssl/-lncurses/-lreadline only when the corresponding ENABLED
  variable is set to true.
- access.html : the default session is now called "id1", not "1".


Revision 5847 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 2 05:19:28 2004 UTC (17 years ago) by nogin
File length: 5514 byte(s)
Diff to previous 5843
More profiling support.


Revision 5843 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 1 20:11:56 2004 UTC (17 years ago) by jyh
File length: 5413 byte(s)
Diff to previous 5797
Updated the OMakefiles to see if we can get threads working again.


Revision 5797 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 20 10:45:43 2004 UTC (17 years, 1 month ago) by nogin
File length: 5904 byte(s)
Diff to previous 5793
Minor clean-up.


Revision 5793 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 19 09:02:14 2004 UTC (17 years, 1 month ago) by nogin
File length: 5885 byte(s)
Diff to previous 5193
A bit more profiling support. Now to get the profile text, one only needs to
enable the NATIVE_PROFILING_ENABLED in mk.config and run
"omake editor/ml/native_profile.txt".


Revision 5193 - (view) (download) (annotate) - [select for diffs]
Modified Thu Dec 18 08:10:31 2003 UTC (17 years, 6 months ago) by nogin
File length: 5679 byte(s)
Diff to previous 5041
(bug 141) Making sure omake gets the dependencies right:

- ocamldep should not denerate .cmi/.cmo: .cmo dependencies when only .ml
file is there, but no .mli is present. Instead, it should just generate the normal
.cmi/.cmo: .cmi dependency (since .cmi is going to be build out of .ml)

- omake can _not_ use "-I $(ROOT)/lib" since things will not be in lib yet at
dependency scan time.

- OCamlGeneratedFiles needs to be redefined for theory files to include .ppo
dependencies.


Revision 5041 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 28 09:01:10 2003 UTC (17 years, 7 months ago) by nogin
File length: 5643 byte(s)
Diff to previous 5035
Use the same ocaml flags in make, omake and prlc compilations.

Check for pa_op.cmo/cmx in addition to camlp4.cma/cmxa (in OCaml 3.07
camlp4.cmxa is there by default, but pa_op.cmx is not :-( ).


Revision 5035 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 24 02:24:37 2003 UTC (17 years, 8 months ago) by nogin
File length: 5628 byte(s)
Diff to previous 5023
- This fixes all-theories.pdf build (bug 57)

- In bytecode mode, omake should use mp.top, not mp.opt

- Made ocamldep -prl mode a bit smarter:
a) When a PRL .mli file contains "mptop", then .cmi dependes on Shell_sig and Mptop
modules
b) When a PRL file contains "interactive", "interactive_rw" or "derived", then it
depeneds on the Shell module
c) All PRL .cmx and .cmo files depend on Shell_sig and Mptop signatures (strictly speaking,
this is only true when the corresponding .mli contains an "mptop" directive), but this is an
approximation

- Printexn.catch is a bad idea now (the runtime now is as good at printing uncaught
exceptions and Printexn.catch blocks exception backtracing), got rid of all of them.

- Print a better error message when trying to cd into a theory that does not exist.

- The all-theories theory list was missing the base_theory file, and the fol_theory one
should not be there.

- Minor changes in module (AKA theory, AKA package) management in shell.

- Made "omake clean" in editor/ml a bit cleaner


Revision 5023 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 22 04:58:47 2003 UTC (17 years, 8 months ago) by nogin
File length: 5628 byte(s)
Diff to previous 4995
Moving shell_http to support/shell, where it belongs.


Revision 4995 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 15 22:57:34 2003 UTC (17 years, 8 months ago) by nogin
File length: 5837 byte(s)
Diff to previous 4986
Renaming config (make/omake) variables:

TESTS -> TESTS_ENABLED
READLINE -> READLINE_ENABLED
NCURSES -> NCURSES_ENABLED

- This makes things more consistent internally
(all the boolean flags are now called *_ENABLED)
- This makes things more consistent with how mcc calls them (and we
want to be able to use MetaPRL's libmojave, which is now the "master" one,
in mcc).


Revision 4986 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 14 04:30:40 2003 UTC (17 years, 8 months ago) by jyh
File length: 5829 byte(s)
Diff to previous 4985
I should name these variables better.


Revision 4985 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 14 04:29:40 2003 UTC (17 years, 8 months ago) by jyh
File length: 5824 byte(s)
Diff to previous 4983
Win32 *really* does not like commands that start with ./ or .\.
For example, ./make_mp_config and .\make_mp_config both do not work.


Revision 4983 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 13 20:59:56 2003 UTC (17 years, 8 months ago) by nogin
File length: 5812 byte(s)
Diff to previous 4982
Ported the new style of mp_version.ml creating back to make system.
Now make works again.


Revision 4982 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 13 09:23:36 2003 UTC (17 years, 8 months ago) by nogin
File length: 5806 byte(s)
Diff to previous 4977
- Fixing the TESTS=YES compilation (again).
- make_mp_version needs a ./ path on Unix.
- No need to clean the tests directory twice.


Revision 4977 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 12 05:49:04 2003 UTC (17 years, 8 months ago) by jyh
File length: 5864 byte(s)
Diff to previous 4976
Adding support for document formatting.

For omake, the new style is to add a dcoumentation command in the
theory, for example, theories/base/OMakefile contains the following:

    #
    # Documentation
    #
    PRINT_THEORIES =\
        base_theory\
        top_tacticals\
        top_conversionals\
        var\
        auto_tactic\
        dtactic\
        base_trivial\
        base_rewrite\
        summary\
        comment\
        mptop

    TheoryDocument(base, $(PRINT_THEORIES))

I still need to get all-theories right, I'll work on it.


Revision 4976 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 11 21:23:50 2003 UTC (17 years, 8 months ago) by jyh
File length: 6257 byte(s)
Diff to previous 4973
Fixed the dependencies for mp_version.ml.  Before, it depended on the byte-code
libraries, causing byte-code to be built even if BYTE_ENABLED=false.


Revision 4973 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 11 17:48:19 2003 UTC (17 years, 8 months ago) by jyh
File length: 6208 byte(s)
Diff to previous 4967
Generate .ppo files.

This adds a new section of rules to the toplevel OMakefile.


Revision 4967 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 11 02:50:41 2003 UTC (17 years, 8 months ago) by jyh
File length: 6352 byte(s)
Diff to previous 4965
emember the generated .o file.


Revision 4965 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 11 02:28:11 2003 UTC (17 years, 8 months ago) by jyh
File length: 6332 byte(s)
Diff to previous 4963
Added the editor/ml/make_mp_version.ml program to *generate* the mp_version.ml
file.  This works, and it may give us extra flexibility in printing the version
string.  However, other solutions that work on win32 and Unix are welcome.

WARNING WARNING WARNING: the Weak module in weak_memo.ml is now enabled.
This hides the weak memo bug, so if you are working on it, be sure to
change the module name to something else.  However, let's leave it like
this in the meantime.  It makes running MetaPRL easier, especially on
win32.


Revision 4963 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 11 00:23:29 2003 UTC (17 years, 8 months ago) by nogin
File length: 6757 byte(s)
Diff to previous 4939
We should always use the proper boolean tests, not $equal(... , YES) ones!
Hopefully, this will also fix the bug 58.


Revision 4939 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 5 15:30:16 2003 UTC (17 years, 9 months ago) by jyh
File length: 6758 byte(s)
Diff to previous 4935
MetaPRL compiles and runs on Cygwin.
Now, I need to figure out the font situation.


Revision 4935 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 5 07:10:12 2003 UTC (17 years, 9 months ago) by nogin
File length: 6702 byte(s)
Diff to previous 4895
- Changed the way mp_version.ml is hapdled to be a -pp hack on a static .ml file.
This will likely break Win32 build! :-(

- Added checks that make sure that the extract passed into Refiner really proves
what it was supposed to prove. This requires moving a HACK that creates sequent
representation of rewrites into the Refine module :-(


Revision 4895 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 29 00:09:07 2003 UTC (17 years, 9 months ago) by nogin
File length: 7266 byte(s)
Diff to previous 4861
This is another major re-arrangement of directories (hopefully,
the last one - at least until we start working on a shared installation mode)
that I've been planning for a while.

Basically, I moved the high-level proof/tactic layer into the tactics top-level
directory (my major objection was that it had absolutely no business being in
filter/boot - the tactic layer has nothing to do with parsing/compiling MetaPRL
files).

In short this, commit moves:
 - filter/boot -> tactics/proof
 - ensemble -> tactics/null, tactics/ensemble (splitting the directory
into separate ones for the distributed and sequential versions).


Revision 4861 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 21 02:51:56 2003 UTC (17 years, 10 months ago) by nogin
File length: 7610 byte(s)
Diff to previous 4853
Moving [o]make variable defaults into a shared file mk/defaults.
This should (more-or-less) fix bug 34.


Revision 4853 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 20 04:34:11 2003 UTC (17 years, 10 months ago) by jyh
File length: 7587 byte(s)
Diff to previous 4725
Added better support for win32.  The main changes are for the C files,
where a lot of support (like readline, ncurses) is missing.


Revision 4725 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 9 08:08:33 2003 UTC (17 years, 11 months ago) by nogin
File length: 7535 byte(s)
Diff to previous 4723
- Got rid of the LIBMOJAVE parameted in mk/config (just always use $(ROOT)/libmojave)
- Converted the theories/experimental/compile to be compatible with the current
incarnation of libmojave


Revision 4723 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 9 07:20:04 2003 UTC (17 years, 11 months ago) by nogin
File length: 7584 byte(s)
Diff to previous 4697
Merging in the abstract_vars branch:
- variables are now an abstract type, not strings
- MVar parameters are gone

See the branch log messages for more information.

P.S. This is a pretty big change, so I bumped the version number
in mk/preface.


Revision 4697 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 4 03:56:03 2003 UTC (17 years, 11 months ago) by jyh
File length: 7818 byte(s)
Diff to previous 4585
Beginning the slow process of migrating MetaPRL toward libmojave.


Revision 4585 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 11 15:09:42 2003 UTC (18 years, 1 month ago) by jyh
File length: 7971 byte(s)
Diff to previous 4565
Added FIR<->term translation.  4000 lines of pure grundge code.


Revision 4565 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 6 03:24:48 2003 UTC (18 years, 1 month ago) by jyh
File length: 7837 byte(s)
Diff to previous 4563
Added more complete version of omake realclean target.  Note, this
migrates the rewrite error to a rule called singleton_elim.


Revision 4563 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 6 02:47:22 2003 UTC (18 years, 1 month ago) by jyh
File length: 7717 byte(s)
Diff to previous 4559
| 1. Fixed the build problem with prlc quitting too early on win32,
|    requiring repeated runs of omake.
|
|    This was actually problem with Unix.execvp, which doesn't
|    work as advertised.  The problem is fixed in prlcomp.ml
|    by using Unix.create_process instead.  I actually ran into
|    this several years ago, and the appropriate code was still
|    around in a comment.
|
| 2. Add some missing .cvsignore entries, since win32 copies
|    files instead of using symbolic links, which don't exist.
|
| 3. Moved infix.ml to infix.win32.ml as discussed with Aleksey.


Revision 4559 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 4 22:11:21 2003 UTC (18 years, 1 month ago) by jyh
File length: 7741 byte(s)
Diff to previous 4549
More minor changes for Win32.  For some reason Itt_collection.isect_wf
gives me a rewrite error at load time...


Revision 4549 - (view) (download) (annotate) - [select for diffs]
Modified Sat May 3 20:26:47 2003 UTC (18 years, 1 month ago) by jyh
File length: 7759 byte(s)
Diff to previous 4548
Ported MetaPRL to native Win32.  The docs for this commit
are in README.WIN32.


Revision 4548 - (view) (download) (annotate) - [select for diffs]
Modified Sat May 3 17:26:35 2003 UTC (18 years, 1 month ago) by jyh
File length: 6166 byte(s)
Diff to previous 4534
Updated omake system to match Aleksey's changes.


Revision 4534 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 1 23:47:36 2003 UTC (18 years, 1 month ago) by nogin
File length: 6403 byte(s)
Diff to previous 4533
The top-level directory for MetaPRL is now supposed to be just "metaprl"
(e.g. without a dash).


Revision 4533 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 1 23:27:28 2003 UTC (18 years, 1 month ago) by jyh
File length: 6403 byte(s)
Diff to previous 4494
Propagate funT changes into theories/experimental/compile.


Revision 4494 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 25 17:52:45 2003 UTC (18 years, 2 months ago) by jyh
File length: 6035 byte(s)
Diff to previous 4439
Some minor changes to the paper.


Revision 4439 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 16 04:10:47 2003 UTC (18 years, 2 months ago) by jyh
File length: 5482 byte(s)
Diff to previous 4433
Added clean and realclean targets.


Revision 4433 - (view) (download) (annotate) - [select for diffs]
Added Tue Apr 15 20:48:46 2003 UTC (18 years, 2 months ago) by jyh
File length: 5446 byte(s)
| Add preliminary omake build system.
|
| Here's some things I haven't done yet.
|    1. Support for some .PHONY targets like "clean".
|    2. TeX compilation needs support in editor/ml/OMakefile.
|    3. Haven't tried "omake -j 4" yet.
|    4. editor/ml/Makefile is pretty ugly, could be cleaned up.


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