FreeBSD Bugzilla – Attachment 108821 Details for
Bug 149736
update port: math/isabelle to version 2009.2
Home
|
New
|
Browse
|
Search
|
[?]
|
Reports
|
Help
|
New Account
|
Log In
Remember
[x]
|
Forgot Password
Login:
[x]
[patch]
files.diff
files.diff (text/plain), 16.16 KB, created by
Timothy Beyer
on 2010-08-17 13:20:01 UTC
(
hide
)
Description:
files.diff
Filename:
MIME Type:
Creator:
Timothy Beyer
Created:
2010-08-17 13:20:01 UTC
Size:
16.16 KB
patch
obsolete
>diff -urN files.orig/patch-etc-settings files/patch-etc-settings >--- files.orig/patch-etc-settings 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-etc-settings 2010-08-16 14:55:01.000000000 -0700 >@@ -1,16 +1,12 @@ >---- etc/settings.orig 2009-10-09 10:34:33.000000000 +1100 >-+++ etc/settings 2009-10-09 10:37:10.000000000 +1100 >-@@ -11,55 +11,11 @@ >- ### ML compiler settings (ESSENTIAL!) >- ### >+--- etc/settings.orig 2010-06-21 02:24:19.000000000 -0700 >++++ etc/settings 2010-08-16 14:53:16.000000000 -0700 >+@@ -15,19 +15,7 @@ >+ # not invent new ML system names unless you know what you are doing. >+ # Only one of the sections below should be activated. > >--# ML_HOME specifies the location of the actual compiler binaries. Do >--# not invent new ML system names unless you know what you are doing. >--# Only one of the sections below should be activated. >-- >--# Poly/ML 4.x/5.x (automated settings) >+-# Poly/ML 5.x (automated settings) > -POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")" >--ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform") >+-ML_PLATFORM="$ISABELLE_PLATFORM" > -ML_HOME=$(choosefrom \ > - "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ > - "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ >@@ -20,48 +16,26 @@ > - $POLY_HOME) > -ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") > -ML_OPTIONS="-H 200" >--ML_DBASE="" >-- >--# Poly/ML 5.1 >--#ML_PLATFORM=x86-linux >--#ML_HOME=/usr/local/polyml/x86-linux >--#ML_SYSTEM=polyml-5.1 >--#ML_OPTIONS="-H 500" >-- >--# Poly/ML 5.1 (64 bit) >--#ML_PLATFORM=x86_64-linux >--#ML_HOME=/usr/local/polyml/x86_64-linux >--#ML_SYSTEM=polyml-5.1 >--#ML_OPTIONS="-H 1000" >-- >--# Poly/ML 4.2.0 >--#ML_PLATFORM=x86-linux >--#ML_HOME=/usr/local/polyml/x86-linux >--#ML_SYSTEM=polyml-4.2.0 >--#ML_OPTIONS="-H 80" >-- >--# Standard ML of New Jersey (slow!) >--#ML_SYSTEM=smlnj-110 >--#ML_HOME="/usr/local/smlnj/bin" >--#ML_OPTIONS="@SMLdebug=/dev/null" >--#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") >--#SMLNJ_CYGWIN_RUNTIME=1 >-- >--# Moscow ML 2.00 (experimental!) >--#ML_SYSTEM=mosml >--#ML_HOME="/usr/local/mosml/bin" >--#ML_OPTIONS="" >--#ML_PLATFORM="" >-- >+-ML_SOURCES="$ML_HOME/../src" >++ >+ >+ # Poly/ML 5.3.0 >+ #ML_PLATFORM=x86-linux >+@@ -50,6 +38,13 @@ >+ #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") >+ #SMLNJ_CYGWIN_RUNTIME=1 >+ >++# FreeBSD PolyML Settings > +ML_SYSTEM=%%ML_SYSTEM%% > +ML_HOME=%%ML_HOME%% > +ML_OPTIONS=%%ML_OPTIONS%% > +ML_PLATFORM=%%ML_PLATFORM%% > +ML_DBASE=%%ML_DBASE%% >++ > > ### > ### JVM components (Scala or Java) >-@@ -81,7 +37,7 @@ >+@@ -64,7 +59,7 @@ > ### Interactive sessions (cf. isabelle tty) > ### > >@@ -70,7 +44,7 @@ > [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" > [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" > >-@@ -131,7 +87,7 @@ >+@@ -109,7 +104,7 @@ > ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" > > # Location for temporary files (should be on a local file system). >@@ -79,7 +53,7 @@ > > # Heap input locations. ML system identifier is included in lookup. > ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps" >-@@ -157,7 +113,7 @@ >+@@ -136,7 +131,7 @@ > ### > > # Where to look for docs (multiple dirs separated by ':'). >@@ -88,7 +62,7 @@ > > # Preferred document format > ISABELLE_DOC_FORMAT=pdf >-@@ -191,9 +147,7 @@ >+@@ -173,9 +168,7 @@ > PROOFGENERAL_HOME=$(choosefrom \ > "$ISABELLE_HOME/contrib/ProofGeneral" \ > "$ISABELLE_HOME/../ProofGeneral" \ >@@ -99,39 +73,20 @@ > "") > > PROOFGENERAL_OPTIONS="" >-@@ -211,9 +165,7 @@ >- JEDIT_HOME=$(choosefrom \ >- "$ISABELLE_HOME/contrib/jedit" \ >- "$ISABELLE_HOME/../jedit" \ >-- "/usr/local/jedit" \ >-- "/usr/share/jedit" \ >-- "/opt/jedit" \ >-+ "%%JAVASHAREDIR%%/jedit" \ >- "") >+@@ -201,9 +194,9 @@ >+ ## Set HOME only for tools you have installed! > >- JEDIT_JAVA_OPTIONS="" >-@@ -231,17 +183,17 @@ >- E_HOME=$(choosefrom \ >- "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \ >- "$ISABELLE_HOME/../E/$ML_PLATFORM" \ >-- "/usr/local/E" \ >-+ "%%PREFIX%%/E" \ >- "") >- VAMPIRE_HOME=$(choosefrom \ >- "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \ >- "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \ >-- "/usr/local/Vampire" \ >-+ "%%PREFIX%%/Vampire" \ >- "") >- SPASS_HOME=$(choosefrom \ >- "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \ >- "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \ >-- "/usr/local/SPASS" \ >-+ "%%PREFIX%%/SPASS" \ >- "") >+ # External provers >+-#E_HOME=/usr/local/bin >+-#SPASS_HOME=/usr/local/bin >+-#VAMPIRE_HOME=/usr/local/bin >++#E_HOME=%%PREFIX%%/bin >++#SPASS_HOME=%%PREFIX%%/bin >++#VAMPIRE_HOME=%%PREFIX%%/bin > > # HOL4 proof objects (cf. Isabelle/src/HOL/Import) >-@@ -253,24 +205,24 @@ >+ #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs" >+@@ -214,24 +207,24 @@ > #SVC_MACHINE=sparc-sun-solaris > > # Mucke (mu-calculus model checker) >@@ -160,5 +115,5 @@ > -#JERUSAT_HOME=/usr/local/bin > +#JERUSAT_HOME=%%PREFIX%%/bin > >- # For configuring HOL/Matrix/cplex >- # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver. >+ # CSDP (SDP Solver, cf. Isabelle/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML) >+ #CSDP_EXE=csdp >diff -urN files.orig/patch-lib-scripts-run_smlnj files/patch-lib-scripts-run_smlnj >--- files.orig/patch-lib-scripts-run_smlnj 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-lib-scripts-run_smlnj 1969-12-31 16:00:00.000000000 -0800 >@@ -1,25 +0,0 @@ >---- lib/scripts/run-smlnj.orig 2009-10-08 20:50:08.000000000 +1100 >-+++ lib/scripts/run-smlnj 2009-10-08 20:51:07.000000000 +1100 >-@@ -38,11 +38,10 @@ >- >- ## compiler binaries >- >-+export SMLNJ_DEVEL=yes >- SML="$ML_HOME/sml" >--ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys" >- >- check_mlhome_file "$SML" >--check_mlhome_file "$ARCH_N_OPSYS" >- >- >- >-@@ -83,8 +82,7 @@ >- ## fix heap file name and permissions >- >- if [ -n "$OUTFILE" ]; then >-- eval $("$ARCH_N_OPSYS") >-- [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS" >-+ [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ML_PLATFORM" >- HEAP="$OUTFILE.$HEAP_SUFFIX" >- check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \ >- [ -n "$NOWRITE" ] && chmod -w "$OUTFILE" >diff -urN files.orig/patch-src-HOL-Tools-atp_manager.ML files/patch-src-HOL-Tools-atp_manager.ML >--- files.orig/patch-src-HOL-Tools-atp_manager.ML 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-src-HOL-Tools-atp_manager.ML 1969-12-31 16:00:00.000000000 -0800 >@@ -1,15 +0,0 @@ >---- src/HOL/Tools/atp_manager.ML.orig 2009-10-18 10:37:58.000000000 +1100 >-+++ src/HOL/Tools/atp_manager.ML 2009-10-18 10:39:46.000000000 +1100 >-@@ -77,9 +77,9 @@ >- fun ord ((a, _), (b, _)) = Time.compare (a, b); >- ); >- >--val lookup_thread = AList.lookup Thread.equal; >--val delete_thread = AList.delete Thread.equal; >--val update_thread = AList.update Thread.equal; >-+fun lookup_thread x = AList.lookup Thread.equal x; >-+fun delete_thread x = AList.delete Thread.equal x; >-+fun update_thread x = AList.update Thread.equal x; >- >- >- (* state of thread manager *) >diff -urN files.orig/patch-src-HOL-Tools-atp_wrapper.ML files/patch-src-HOL-Tools-atp_wrapper.ML >--- files.orig/patch-src-HOL-Tools-atp_wrapper.ML 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-src-HOL-Tools-atp_wrapper.ML 1969-12-31 16:00:00.000000000 -0800 >@@ -1,18 +0,0 @@ >---- src/HOL/Tools/atp_wrapper.ML.orig 2009-10-18 11:13:04.000000000 +1100 >-+++ src/HOL/Tools/atp_wrapper.ML 2009-10-18 11:14:20.000000000 +1100 >-@@ -112,13 +112,13 @@ >- fun tptp_prover_opts max_new theory_const = >- tptp_prover_opts_full max_new theory_const false; >- >--val tptp_prover = tptp_prover_opts 60 true; >-+fun tptp_prover x = tptp_prover_opts 60 true x; >- >- (*for structured proofs: prover must support TSTP*) >- fun full_prover_opts max_new theory_const = >- tptp_prover_opts_full max_new theory_const true; >- >--val full_prover = full_prover_opts 60 true; >-+fun full_prover x = full_prover_opts 60 true x; >- >- >- (* Vampire *) >diff -urN files.orig/patch-src-HOL-Tools-int_arith.ML files/patch-src-HOL-Tools-int_arith.ML >--- files.orig/patch-src-HOL-Tools-int_arith.ML 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-src-HOL-Tools-int_arith.ML 1969-12-31 16:00:00.000000000 -0800 >@@ -1,29 +0,0 @@ >---- src/HOL/Tools/int_arith.ML.orig 2009-04-17 01:29:56.000000000 +1000 >-+++ src/HOL/Tools/int_arith.ML 2009-10-17 19:35:35.000000000 +1100 >-@@ -229,7 +229,7 @@ >- val mk_coeff = mk_coeff >- val dest_coeff = dest_coeff 1 >- val find_first_coeff = find_first_coeff [] >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- fun norm_tac ss = >- ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) >-@@ -308,7 +308,7 @@ >- val dest_coeff = dest_coeff 1 >- val left_distrib = @{thm combine_common_factor} RS trans >- val prove_conv = Arith_Data.prove_conv_nohyps >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- fun norm_tac ss = >- ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) >-@@ -334,7 +334,7 @@ >- val dest_coeff = dest_fcoeff 1 >- val left_distrib = @{thm combine_common_factor} RS trans >- val prove_conv = Arith_Data.prove_conv_nohyps >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps >- fun norm_tac ss = >diff -urN files.orig/patch-src-HOL-Tools-int_factor_simprocs.ML files/patch-src-HOL-Tools-int_factor_simprocs.ML >--- files.orig/patch-src-HOL-Tools-int_factor_simprocs.ML 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-src-HOL-Tools-int_factor_simprocs.ML 1969-12-31 16:00:00.000000000 -0800 >@@ -1,65 +0,0 @@ >---- src/HOL/Tools/int_factor_simprocs.ML.orig 2009-10-17 19:46:40.000000000 +1100 >-+++ src/HOL/Tools/int_factor_simprocs.ML 2009-10-17 20:06:01.000000000 +1100 >-@@ -29,7 +29,7 @@ >- struct >- val mk_coeff = mk_coeff >- val dest_coeff = dest_coeff 1 >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s >- val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps >-@@ -249,7 +249,7 @@ >- val mk_coeff = mk_coeff >- val dest_coeff = dest_coeff >- val find_first = find_first_t [] >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} >- fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) >- val simplify_meta_eq = cancel_simplify_meta_eq >-@@ -261,7 +261,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_eq >- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT >-- val simp_conv = K (K (SOME @{thm mult_cancel_left})) >-+ fun simp_conv _ _ = SOME @{thm mult_cancel_left} >- ); >- >- (*for ordered rings*) >-@@ -290,7 +290,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binop @{const_name Divides.div} >- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT >-- val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if})) >-+ fun simp_conv _ _ = SOME @{thm zdiv_zmult_zmult1_if} >- ); >- >- structure IntModCancelFactor = ExtractCommonTermFun >-@@ -298,7 +298,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} >- val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT >-- val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1})) >-+ fun simp_conv _ _ = SOME @{thm zmod_zmult_zmult1} >- ); >- >- structure IntDvdCancelFactor = ExtractCommonTermFun >-@@ -306,7 +306,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} >- val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT >-- val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) >-+ fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} >- ); >- >- (*Version for all fields, including unordered ones (type complex).*) >-@@ -315,7 +315,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} >- val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT >-- val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) >-+ fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} >- ); >- >- val cancel_factors = >diff -urN files.orig/patch-src-HOL-Tools-nat_simprocs.ML files/patch-src-HOL-Tools-nat_simprocs.ML >--- files.orig/patch-src-HOL-Tools-nat_simprocs.ML 2009-10-29 15:23:28.000000000 -0700 >+++ files/patch-src-HOL-Tools-nat_simprocs.ML 1969-12-31 16:00:00.000000000 -0800 >@@ -1,83 +0,0 @@ >---- src/HOL/Tools/nat_simprocs.ML.orig 2009-10-17 19:48:52.000000000 +1100 >-+++ src/HOL/Tools/nat_simprocs.ML 2009-10-18 09:59:34.000000000 +1100 >-@@ -142,7 +142,7 @@ >- val mk_coeff = mk_coeff >- val dest_coeff = dest_coeff >- val find_first_coeff = find_first_coeff [] >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ >- [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} >-@@ -231,7 +231,7 @@ >- val dest_coeff = dest_coeff >- val left_distrib = @{thm left_add_mult_distrib} RS trans >- val prove_conv = Arith_Data.prove_conv_nohyps >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac} >- val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} >-@@ -256,7 +256,7 @@ >- struct >- val mk_coeff = mk_coeff >- val dest_coeff = dest_coeff >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- >- val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps >- numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} >-@@ -362,7 +362,7 @@ >- val mk_coeff = mk_coeff >- val dest_coeff = dest_coeff >- val find_first = find_first_t [] >-- val trans_tac = K Arith_Data.trans_tac >-+ fun trans_tac _ = Arith_Data.trans_tac >- val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} >- fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) >- val simplify_meta_eq = cancel_simplify_meta_eq >-@@ -373,7 +373,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_eq >- val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT >-- val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj})) >-+ fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj} >- ); >- >- structure LessCancelFactor = ExtractCommonTermFun >-@@ -381,7 +381,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} >- val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT >-- val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj})) >-+ fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} >- ); >- >- structure LeCancelFactor = ExtractCommonTermFun >-@@ -389,7 +389,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} >- val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT >-- val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj})) >-+ fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} >- ); >- >- structure DivideCancelFactor = ExtractCommonTermFun >-@@ -397,7 +397,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binop @{const_name Divides.div} >- val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT >-- val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj})) >-+ fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj} >- ); >- >- structure DvdCancelFactor = ExtractCommonTermFun >-@@ -405,7 +405,7 @@ >- val prove_conv = Arith_Data.prove_conv >- val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} >- val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT >-- val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj})) >-+ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} >- ); >- >- val cancel_factor =
You cannot view the attachment while viewing its details because your browser does not support IFRAMEs.
View the attachment on a separate page
.
View Attachment As Diff
View Attachment As Raw
Actions:
View
|
Diff
Attachments on
bug 149736
:
108820
| 108821 |
108822