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

Log of /metaprl/mk/defaults

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 9641 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 28 15:28:01 2006 UTC (14 years, 7 months ago) by nogin
File length: 3639 byte(s)
Diff to previous 9418
MetaPRL is compatible with OCaml 3.09.3


Revision 9418 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 4 23:54:21 2006 UTC (14 years, 11 months ago) by nogin
File length: 3632 byte(s)
Diff to previous 9252
Include the words file in the distribution so that we do not need to worry
about different setups having very different words files (or no words file at
all). This version of the words.linux file is a copy of the linux.words file
from Red Hat's words-3.0-3 package, which in turn took the file from
http://www.dcs.shef.ac.uk/research/ilash/Moby/.

Also, removed a number of words from words.metaprl as they now appear in the
words.linux.

P.S. According to both the package and the above URL, the file is in public
domain.


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


Revision 9229 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 31 21:55:36 2006 UTC (15 years ago) by jyh
File length: 3399 byte(s)
Diff to previous 9173
Removed ocaml_doc.  It has been moved to plain LaTeX in the papers
directory.


Revision 9173 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 10 23:30:05 2006 UTC (15 years, 1 month ago) by nogin
File length: 3409 byte(s)
Diff to previous 9021
MetaPRL is compatible with OCaml 3.09.2


Revision 9021 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 5 03:29:10 2006 UTC (15 years, 2 months ago) by jyh
File length: 3402 byte(s)
Diff to previous 8617
Some progress on sequent normalization.


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: 3416 byte(s)
Diff to previous 8599
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 8599 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 25 02:22:58 2006 UTC (15 years, 4 months ago) by jyh
File length: 2826 byte(s)
Diff to previous 8598
We're back in business in PoplMark, at least for the first three
term declarations.

Sequents are now BTerms.

I adopted a new normalization style in Itt_hoas_sequent_term.
This means we have some junk theorems there, and it is confusing.
Will try Aleksey's method of check_all next.


Revision 8598 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 23:08:04 2006 UTC (15 years, 4 months ago) by jyh
File length: 2811 byte(s)
Diff to previous 8579
Try to be more careful about using length{vlist{| <J> |}} as
the canonical expression for the length of a context.

Temporarily remove poplmark/naive from THEORIES_ALL until
the proofs terminate.


Revision 8579 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jan 24 02:42:12 2006 UTC (15 years, 5 months ago) by nogin
File length: 2825 byte(s)
Diff to previous 8545
Made the default browser command configurable via the mk/config.


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: 2712 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: 2701 byte(s)
Diff to previous 8530
- 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 8530 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 05:34:28 2006 UTC (15 years, 5 months ago) by nogin
File length: 2408 byte(s)
Diff to previous 8529
Made it possible to actually change the THEORY_PATH variable.


Revision 8529 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 20 04:59:26 2006 UTC (15 years, 5 months ago) by jyh
File length: 2391 byte(s)
Diff to previous 8528
Add a THEORYPATH search path for theories.

Note: the theories in the install directory have
the READONLY=true flag appended to their MetaprlInfo
file, so they will not get compiled, just
noticed.

However, a user can put his theories in various
other places.  If the .dir files work, it should be no
problem (untested).


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: 2361 byte(s)
Diff to previous 8424
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 8424 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 7 19:36:28 2006 UTC (15 years, 5 months ago) by nogin
File length: 1835 byte(s)
Diff to previous 8418
Adding poplmark/naive to the "THEORIES=all" list.


Revision 8418 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 7 05:31:31 2006 UTC (15 years, 5 months ago) by nogin
File length: 1820 byte(s)
Diff to previous 8330
- Itt_nat should extend Itt_omega

- Now that "meta" is a virtual theory (that is needed for "omake doc"), it
  needs to be listed explicitly in THEORIES_ALL (in mk/defaults)


Revision 8330 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 20 19:09:50 2005 UTC (15 years, 6 months ago) by nogin
File length: 1815 byte(s)
Diff to previous 8261
- Added a "DEFAULT_UI" variable to the mk/config file, with possible values:
  "browser" (default) and "cli".
  
- Also added a "-browser" command-line option. Of course, -browser/-cli
  command line options (which are exclusive) have higher precedence thatn
  DEFAULT_UI. The DEFAULT_UI is only consulted when neither of the two
  command-line options are given.

- Simplified some of the WrapC/PrlC/procomp setup, adding value dependencies
  to make it more precise.

- Added pa_macro to MetaPRL filter. Now we can use structured IFDEFs in the
  MetaPRL files.


Revision 8261 - (view) (download) (annotate) - [select for diffs]
Modified Sun Dec 4 04:00:26 2005 UTC (15 years, 6 months ago) by nogin
File length: 1794 byte(s)
Diff to previous 8127
Change the parse-time representation of the "default context dependencies" to
be v<|!!|> (two exclamation signs) instead of v<|v|>.


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: 1794 byte(s)
Diff to previous 8046
(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 8046 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 29 18:29:43 2005 UTC (15 years, 7 months ago) by nogin
File length: 1804 byte(s)
Diff to previous 8024
MetaPRL is now compatible with OCaml 3.09 (while retaining compatibility with
3.08).


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: 1660 byte(s)
Diff to previous 7956
- 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 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: 1638 byte(s)
Diff to previous 7951
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 7951 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 21 02:09:17 2005 UTC (15 years, 8 months ago) by jyh
File length: 1656 byte(s)
Diff to previous 7932
Group/VNC editing (Aleksey, Alexei, Jason and Xin):

This refactors ITT into several subdirectories instead of a single huge pile
that we used to have.


Revision 7932 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 19 05:42:47 2005 UTC (15 years, 8 months ago) by yegor
File length: 1651 byte(s)
Diff to previous 7836
Ocaml 3.08.0 and 3.08.1 are not good enough - they don't have Pcaml.position needed to compile util/pa_macro.ml

Revision 7836 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 4 13:16:52 2005 UTC (15 years, 8 months ago) by nogin
File length: 1665 byte(s)
Diff to previous 7834
Before changing to editor/ml, set MP_CWD environment variable to point to the
wd where the MetaPRL script was originally started from.


Revision 7834 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 4 04:12:08 2005 UTC (15 years, 8 months ago) by nogin
File length: 1663 byte(s)
Diff to previous 7710
Bumping the version number (to account for Ignore-related changes).


Revision 7710 - (view) (download) (annotate) - [select for diffs]
Modified Thu Sep 15 08:36:29 2005 UTC (15 years, 9 months ago) by nogin
File length: 1663 byte(s)
Diff to previous 7682
Use configure for readline/ncurses.


Revision 7682 - (view) (download) (annotate) - [select for diffs]
Modified Fri Aug 26 22:21:55 2005 UTC (15 years, 9 months ago) by nogin
File length: 1619 byte(s)
Diff to previous 7679
Bumping the MP_VERSION from 0.9.6.1+ to 0.9.6.2+


Revision 7679 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 17 00:06:35 2005 UTC (15 years, 10 months ago) by nogin
File length: 1619 byte(s)
Diff to previous 7580
NetaPRL is compatible with OCaml 3.08.4


Revision 7580 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 12 01:11:31 2005 UTC (15 years, 11 months ago) by yegor
File length: 1612 byte(s)
Diff to previous 7415
S4 is working again.
Now I have to test multi-modal behavior.
I also added S4LP to the "theories=all" list


Revision 7415 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 26 20:27:06 2005 UTC (15 years, 11 months ago) by nogin
File length: 1607 byte(s)
Diff to previous 7261
- Fill reasonable defaults for TERMS, REFINER, etc (instead of "undefined"),
  making it possible to use the initial default mk/config without changes
  (provided "THEORIES = base itt" is what one wants).

- Give a better message when a new mk/config is created. Will work best with
  omake >= 0.9.4.24


Revision 7261 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 12 06:14:16 2005 UTC (16 years, 1 month ago) by nogin
File length: 1616 byte(s)
Diff to previous 7237
Removing some leftover Phobos stuff.


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: 1623 byte(s)
Diff to previous 7142
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 7142 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 5 19:30:28 2005 UTC (16 years, 2 months ago) by jyh
File length: 1588 byte(s)
Diff to previous 7140
Move the config to the compiler-specific directories.


Revision 7140 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 5 18:46:46 2005 UTC (16 years, 2 months ago) by jyh
File length: 1668 byte(s)
Diff to previous 6971
This is the bare template for pmc, which is completely empty right
now, but at least it compiles:)


Revision 6971 - (view) (download) (annotate) - [select for diffs]
Modified Fri Mar 18 08:10:54 2005 UTC (16 years, 3 months ago) by nogin
File length: 1628 byte(s)
Diff to previous 6790
MetaPRL is compatible with OCaml 3.08.3

P.S. The RPMs of the new OCaml are available at
http://rpm.nogin.org/ocaml.html


Revision 6790 - (view) (download) (annotate) - [select for diffs]
Modified Tue Mar 1 23:09:16 2005 UTC (16 years, 3 months ago) by jyh
File length: 1621 byte(s)
Diff to previous 6566
Use omake to construct the final mmc theory.

In mk/config, you now have the option to specify the
mmc extensions and backends.

For each extension, you must specify:
   1. The name of the extension
   2. The files
   3. Any backend-specific files

See any of the extensions/*/Files for examples.


Revision 6566 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 2 21:43:35 2005 UTC (16 years, 4 months ago) by jyh
File length: 1581 byte(s)
Diff to previous 6355
The standalone libmojave was forgetting all INCLUDES, so
ssl was not being included on Win32.


Revision 6355 - (view) (download) (annotate) - [select for diffs]
Modified Fri Dec 10 20:58:52 2004 UTC (16 years, 6 months ago) by nogin
File length: 1578 byte(s)
Diff to previous 6289
Moved the SSL_WIN32 stuff to mk/defaults so that it can still be overridden
in mk/config.local


Revision 6289 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 24 23:53:48 2004 UTC (16 years, 6 months ago) by nogin
File length: 1353 byte(s)
Diff to previous 6179
MetaPRL works fine with 3.08.2 (no special patches needed).


Revision 6179 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 6 22:21:43 2004 UTC (16 years, 9 months ago) by nogin
File length: 1346 byte(s)
Diff to previous 6104
Added a patch for 3.08.1 to make it work with MetaPRL.


Revision 6104 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 21 20:03:52 2004 UTC (16 years, 11 months ago) by jyh
File length: 1339 byte(s)
Diff to previous 6091
Some formatting changes.


Revision 6091 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 15 04:01:49 2004 UTC (16 years, 11 months ago) by nogin
File length: 1325 byte(s)
Diff to previous 6081
- Got rid of the annoying _DEFAULT suffix.
- On Windows, do not include the ignored variables (NCURSES, etc) in mk/config
- Try turning the booleans in mk/config to canonical true/false values.


Revision 6081 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 14 21:27:10 2004 UTC (16 years, 11 months ago) by nogin
File length: 1154 byte(s)
Diff to previous 6076
***************************************************************************
* WARNING: With this commit MetaPRL now requires OCaml 3.08 and OMake 0.8 *
***************************************************************************

This commit:
- Updates MetaPRL to be compatible with OCaml 3.08 (some of the code for
handling the new "position" type is still half-baked, waiting for the
resolution of bug 256.
- Moves the "C:\ocaml\lib" default into mk/defaults.
- Removes references to mk/make_config.sh from mk/make_config


Revision 6076 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 14 20:19:21 2004 UTC (16 years, 11 months ago) by nogin
File length: 1047 byte(s)
Diff to previous 6023
In preparation for 3.06 -> 3,08 switch, I am calling this MetaPRL version 0.9.6.1


Revision 6023 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 25 03:34:43 2004 UTC (17 years ago) by nogin
File length: 1046 byte(s)
Diff to previous 6020
The MetaPRL trunk is now version 0.9.6+


Revision 6020 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 25 03:23:02 2004 UTC (17 years ago) by nogin
File length: 1046 byte(s)
Diff to previous 5970
Removing the make build system. Now the only way to build MetaPRL
is to use omake!


Revision 5970 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 05:29:35 2004 UTC (17 years ago) by nogin
File length: 1135 byte(s)
Diff to previous 5843
- I've changed the browser interface to be the default one. Use the "-cli"
option to get the command-line interface (mpxterm and mpkonsole scripts
will set the -cli flag automatically).
- The SSL and THREADS will now be enabled by default (this only has effects
when you do _not_ already have an mk/config)


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


Revision 5822 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 28 06:03:51 2004 UTC (17 years ago) by jyh
File length: 1107 byte(s)
Diff to previous 5820
SSL should be off by default.


Revision 5820 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 28 02:00:18 2004 UTC (17 years ago) by jyh
File length: 1099 byte(s)
Diff to previous 5708
This is the browser update I've been putting off.
   1. Browser now support both Mozilla *and* IE.
      I haven't tested on others like Safari.
      To get this to work, I had to use iframes
      and code custom menus.  Bleh.
   2. Connections are now SSL.  That is, you need to
      use https: connections instead of http:
   3. File editing is partially supported.  By default
      you edit in the browser.  However, you can define
      the application/x-metaprl MIME type to invoke
      an external editor.

      This is the main reason for using SSL.  At some
      point, we should do a code review to make sure
      we believe the security model
      (MD5 challenge/response).

TODO:
   1. Currently, edited files are not saved.  This is
      just a precaution for the moment.
   2. Need to add make/restart commands.  Easy, just
      haven't done it yet.

NOTE: I haven't checked that win32 compiles.  Working on that
next.


Revision 5708 - (view) (download) (annotate) - [select for diffs]
Modified Sat Apr 24 02:18:02 2004 UTC (17 years, 2 months ago) by jyh
File length: 1081 byte(s)
Diff to previous 5668
Remove aggressive use of Lm_rformat.  To use the normal format library,
use Lm_printf.  For output that should be diverted to the output device,
use Lm_rprintf.


Revision 5668 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 01:46:53 2004 UTC (17 years, 2 months ago) by jyh
File length: 1106 byte(s)
Diff to previous 5605
This is an annoying commit.  It looks massive, but many of the changes
are just to "open" statements.  Here is the issue that is addressed.
   1. Format is a superset of Printf, and it is much better.
   2. MetaPRL's Rformat is a superset of Format, and it is much better.

This commit moves Rformat into libmojave, as Lm_rformat.  With this
commit, all output normally goes through Lm_rformat.  Feel free to
continue to use Format/Printf in special cases, but normal user output
should go through Lm_format/Lm_printf.  You will probably need to use
Lm_pervasives as well.

Lm_pervasives defines an (output_rbuffer : out_channel -> Lm_buffer.t -> unit)
that should be used instead of the print_text_channel function.

There is a new FORMAT option in mk/config.  Define FORMAT=Format to
enable old behavior if you have trouble.

There are two reasons behind this:
   1. We had a mix of files that use Printf and those that use Format
      for output.  This was a mess.  For instance format-style print
      directives (like "@[<hv 3>Content of text box@]@.") can't be
      used in raw Printf.  This meant that output functions had
      to be duplicated, one version for Printf, and one for Format.
      This commit solves the problem.
   2. Another reason, and the real reason behind this, is to allow
      output to be diverted based on the display device.


Revision 5605 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 6 00:20:23 2004 UTC (17 years, 2 months ago) by nogin
File length: 1081 byte(s)
Diff to previous 5306
The theories/mojave now lives in a separate CVS repository "mmc" on cvs.metaprl.org.

I am not quite sure, but I believe that "mmc" is supposed to stand for something like
"Mojave Meta-Compiler", "Meta Mojave Compiler", "Modern Mojave Compiler", or
"Mean Meta-Compiler" ;-)

The commit logs for the "mmc" repository are going to go to mcc-cvs@metaprl.org,
go to https://lists.metaprl.org/mailman/listinfo/mcc-cvs to subscribe.


Revision 5306 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 28 20:00:08 2004 UTC (17 years, 4 months ago) by nogin
File length: 1046 byte(s)
Diff to previous 5276
Adding support for native code profiling to omake.


Revision 5276 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jan 26 09:00:53 2004 UTC (17 years, 4 months ago) by nogin
File length: 1025 byte(s)
Diff to previous 5271
Use "-inline 3" when compiling to native code.


Revision 5271 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jan 23 00:03:18 2004 UTC (17 years, 5 months ago) by nogin
File length: 963 byte(s)
Diff to previous 5270
- In the previous commit, forgot to actually drop mesa and kat theories
from the list

- Removing couple of unused files.


Revision 5270 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 22 23:04:48 2004 UTC (17 years, 5 months ago) by nogin
File length: 972 byte(s)
Diff to previous 5269
- Added omake support to theories/kat
- For now, do not include kat and mesa in THEORIES=all (and nightly status checks) -
they are pretty big theories, but do not have much proofs yet.


Revision 5269 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jan 22 06:08:47 2004 UTC (17 years, 5 months ago) by nogin
File length: 924 byte(s)
Diff to previous 5121
- Adding the MESA theory to "THEORIES=all"
- Adding an anchor to the "Simplified syntax" section of mp-terms.html
- Other minor fixes.


Revision 5121 - (view) (download) (annotate) - [select for diffs]
Modified Tue Nov 25 23:55:10 2003 UTC (17 years, 6 months ago) by nogin
File length: 919 byte(s)
Diff to previous 5041
- (bug 45) in "cvs realclean", skip .omakedb, mk/config and mk/config.local
- (bug 106) check CAMLLIB, OCAMLLIB and CAMLP4LIB environment variables


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: 963 byte(s)
Diff to previous 4995
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 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: 924 byte(s)
Diff to previous 4947
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 4947 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 6 01:15:18 2003 UTC (17 years, 9 months ago) by nogin
File length: 913 byte(s)
Diff to previous 4945
The version 0.9.5 is now tagged with CVS tag "metaprl_0_9_5" and I am
changing the version string to 0.9.5+ to make sure that only this exact
version of MetaPRL calls itself 0.9.5.


Revision 4945 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 6 01:06:59 2003 UTC (17 years, 9 months ago) by nogin
File length: 912 byte(s)
Diff to previous 4940
Version 0.9.5!!!


Revision 4940 - (view) (download) (annotate) - [select for diffs]
Modified Fri Sep 5 17:37:53 2003 UTC (17 years, 9 months ago) by nogin
File length: 912 byte(s)
Diff to previous 4928
Extraction finally works!!!!!!!!!!


Revision 4928 - (view) (download) (annotate) - [select for diffs]
Modified Thu Sep 4 04:11:28 2003 UTC (17 years, 9 months ago) by jyh
File length: 912 byte(s)
Diff to previous 4861
Implemented versioning, check_config, etc.

CAUTION: you will need the latest version of omake to do this, since
it defines new functions needed during versioning.


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


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