/[mojave]/metaprl/OMakefile_common
ViewVC logotype

Log of /metaprl/OMakefile_common

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: 12812 byte(s)
Diff to previous 9494
Made MetaPRL compile with the latest 0.9.8 OMake.


Revision 9494 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 13 22:27:12 2006 UTC (14 years, 10 months ago) by jyh
File length: 12531 byte(s)
Diff to previous 9259
On Win32, the OpenSSL libraries have been renamed.

Be sure to escape the browser path on  Win32 (because
it contains \ characters).


Revision 9259 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 6 21:11:26 2006 UTC (15 years ago) by nogin
File length: 12519 byte(s)
Diff to previous 9256
Simplified the clean rules and made them 0.9.8-compatible.


Revision 9256 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 6 01:02:22 2006 UTC (15 years ago) by nogin
File length: 12549 byte(s)
Diff to previous 9252
I am not sure what the "-$'(RM) ..." syntax used to do, but in 0.9.8 OMake no
longer does anything special for this "-" and just complains that it can not
execute "-rm", so I am removing the "-".


Revision 9252 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 5 22:37:25 2006 UTC (15 years ago) by nogin
File length: 12551 byte(s)
Diff to previous 9047
- Fixed spelling errors in documentation.
- Enable spell-checking by default.


Revision 9047 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 11 02:52:51 2006 UTC (15 years, 2 months ago) by nogin
File length: 12288 byte(s)
Diff to previous 8896
Require OMake 0.9.6.9


Revision 8896 - (view) (download) (annotate) - [select for diffs]
Modified Thu Mar 16 03:39:05 2006 UTC (15 years, 3 months ago) by jyh
File length: 12288 byte(s)
Diff to previous 8772
Changes for compiling with strict quoting.
The changes are backwards-compatible.


Revision 8772 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 22 04:05:06 2006 UTC (15 years, 4 months ago) by jyh
File length: 12298 byte(s)
Diff to previous 8617
This version, rather than having Reflect_foo extend Foo,
just copies the terms from Foo into Reflect_foo verbatim.

Otherwise, there is no logical relation between the
theories.


Revision 8617 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 27 22:25:14 2006 UTC (15 years, 4 months ago) by nogin
File length: 12292 byte(s)
Diff to previous 8597
Moving the settings of the OMake variables to mk/default. This way, mk/config
rules are in scope of the OMakeFlags and their execution would not be
unnecessarily verbose.


Revision 8597 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 22:38:37 2006 UTC (15 years, 4 months ago) by nogin
File length: 12882 byte(s)
Diff to previous 8593
- Better scoping of build options.

- Added a HACKish list of files that depend on $(BIN) and $(LIB) directories
  (This is not needed with the change I just made in OMake, but needed with
  OMake 0.9.6.8).


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: 12949 byte(s)
Diff to previous 8577
- 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 8577 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 23 22:47:41 2006 UTC (15 years, 5 months ago) by nogin
File length: 12911 byte(s)
Diff to previous 8545
- MetaPRL (especially the read-only mode) requires OMake 0.9.6.8
- Debugging code in reduceC was broken.


Revision 8545 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 21 04:59:16 2006 UTC (15 years, 5 months ago) by jyh
File length: 13005 byte(s)
Diff to previous 8543
The new patch for check OCaml versions was breaking because
the installation in the $(INSTALL_DIR) has a different shape
than $(MP_ROOT).  In particular it was $(INSTALL_DIR)/lib/mk
vs $(MP_ROOT)/mk.

Since this is a general headache, I readjusted mp.install to use the
following dirs:
   lib bin export/mk export/theories
and installed into $(INSTALL_DIR)/
   lib bin mk theories

Also:
   - Fixed THEORYPATH, it should include $(INSTALL_DIR)/theories,
     not $(INSTALL_DIR).

   - Removed READONLY theories from the set of build directories.

IMHO, we should "clean" the lib/ directory so it does not contain
any real files (right now it contains just the lib/words file).
This would make our clean scripts easier.  In fact, ideally,
we would remove lib/ and bin/ from svn entirely.

I think that this would just require a change to OCaml.om, where
OCamlLibraryCopy files would depend on $(LIB), etc.  This would usually
have no effect, but users could define a rule that would mkdir the $(LIB)
and $(BIN) directories it if they do not exist.


Revision 8543 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 21 02:58:35 2006 UTC (15 years, 5 months ago) by nogin
File length: 12464 byte(s)
Diff to previous 8535
- MetaPRL is compatible with OCaml 3.09.1

- When using the shared installation mode (I've added a SHARED_MODE variable),
  users have to use the exact same version of OCaml as the one that was used
  for the initial shared build.


Revision 8535 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 07:27:33 2006 UTC (15 years, 5 months ago) by jyh
File length: 11885 byte(s)
Diff to previous 8532
At this point, I'm just tweaking the config.

It turns out, we need to install the .cmoz files too,
or else "cd" into a theory will fail if there is no .prla.


Revision 8532 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 05:43:01 2006 UTC (15 years, 5 months ago) by jyh
File length: 11895 byte(s)
Diff to previous 8528
OCAMLINCLUDES[] was computed incorrectly in the Theory(files) function.


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: 11192 byte(s)
Diff to previous 8518
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 8518 - (view) (download) (annotate) - [select for diffs]
Added Thu Jan 19 22:03:05 2006 UTC (15 years, 5 months ago) by jyh
File length: 11166 byte(s)
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.


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