/[mojave]/metaprl/mk/make_config.sh
ViewVC logotype

Log of /metaprl/mk/make_config.sh

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 6077)

Revision 3591 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 2716 byte(s)
Diff to previous 3419
- 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 3419 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Sat Oct 6 01:40:01 2001 UTC (19 years, 8 months ago) by nogin
File length: 2678 byte(s)
Diff to previous 3039
- 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 3039 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Fri Aug 4 17:28:59 2000 UTC (20 years, 10 months ago) by nogin
File length: 2545 byte(s)
Diff to previous 3038
Even shorter URLs:
http://cvs.metaprl.org:12000/cvsweb/~checkout~/meta-prl/doc/htmlman/... ->
http://cvs.metaprl.org:12000/metaprl/...


Revision 3038 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Fri Aug 4 07:43:46 2000 UTC (20 years, 10 months ago) by nogin
File length: 2607 byte(s)
Diff to previous 3030
ensemble01.cs.cornell.edu -> cvs.metaprl.org


Revision 3030 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Tue Jul 25 17:22:43 2000 UTC (20 years, 11 months ago) by nogin
File length: 2630 byte(s)
Diff to previous 3029
TODO - ocamldebug and ocamlprof support.


Revision 3029 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Fri Jul 21 00:58:24 2000 UTC (20 years, 11 months ago) by jyh
File length: 2612 byte(s)
Diff to previous 2995
Added readline input handling.


Revision 2995 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Tue May 30 05:28:42 2000 UTC (21 years ago) by nogin
File length: 2530 byte(s)
Diff to previous 2994
Moved Jprover output parsing into the JLogic interface. Still need to write the
output parsing for ITT_JLogic.

Eliminated some excessive whitespace from jall.ml

Eliminated some unnecessary exception handling code from jall.ml


Revision 2994 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Tue May 30 03:55:15 2000 UTC (21 years ago) by nogin
File length: 2531 byte(s)
Diff to previous 2906
I wrote several sections of MetaPRL Developer Guide.

Please take a look at it at
http://ensemble01.cs.cornell.edu:12000/cvsweb/~checkout~/meta-prl/doc/htmlman/default.html


Revision 2906 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Tue Feb 22 17:42:16 2000 UTC (21 years, 4 months ago) by jyh
File length: 2231 byte(s)
Diff to previous 2889
Itt_bool now expands.


Revision 2889 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Fri Feb 18 03:26:38 2000 UTC (21 years, 4 months ago) by nogin
File length: 2235 byte(s)
Diff to previous 2850
- 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 2850 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Tue Nov 16 07:11:24 1999 UTC (21 years, 7 months ago) by nogin
File length: 2161 byte(s)
Diff to previous 2777
Added a warning about make 3.77 doing something wrong w.r.t dependencies


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


Revision 2775 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 1982 byte(s)
Diff to previous 2747
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 2747 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Wed Jun 23 23:40:57 1999 UTC (22 years ago) by nogin
File length: 1704 byte(s)
Diff to previous 2745
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 2745 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Wed Jun 23 22:19:48 1999 UTC (22 years ago) by nogin
File length: 1657 byte(s)
Diff to previous 2661
Updated the ds/std and VERBOSE/SIMPLE documentation.

Updated mk/make_config.sh to include in mk/config the pointers to this documentation


Revision 2661 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Fri May 21 01:22:28 1999 UTC (22 years, 1 month ago) by nogin
File length: 1551 byte(s)
Diff to previous 2657
- Updated the BUGS file

Changes suggested by Carl R. Witty <cwitty@newtonlabs.com>:
- Give better error message when $(OSTYPE) is unknown
- Added comments to mk/config telling that the file is generated


Revision 2657 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Thu May 20 20:45:26 1999 UTC (22 years, 1 month ago) by nogin
File length: 1179 byte(s)
Diff to previous 2656
Make sure OCAMLSRC and ENSROOT are non-empty


Revision 2656 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Wed May 19 21:08:40 1999 UTC (22 years, 1 month ago) by jyh
File length: 1138 byte(s)
Diff to previous 2637
The rule for induction on W-types was unsound.  Fix thanks
to Carl Witty <cwitty@newtonlabs.com>.


Revision 2637 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Tue Apr 6 23:29:52 1999 UTC (22 years, 2 months ago) by nogin
File length: 1255 byte(s)
Diff to previous 2622
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 2622 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Sat Mar 20 05:55:17 1999 UTC (22 years, 3 months ago) by nogin
File length: 691 byte(s)
Diff to previous 2621
Fixed a typo


Revision 2621 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Fri Mar 19 06:18:45 1999 UTC (22 years, 3 months ago) by nogin
File length: 692 byte(s)
Diff to previous 2590
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 2590 - (view) (download) (as text) (annotate) - [select for diffs]
Added Fri Feb 12 23:50:37 1999 UTC (22 years, 4 months ago) by nogin
File length: 650 byte(s)
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"


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