From e4267f5c1f0df789cb1ed912638e0dc6ca52baf3 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Wed, 14 Sep 2011 15:35:01 +0200 Subject: [PATCH] Task checksum does not depend on Pretty anymore --- examples/bts/12475/why3session.xml | 17 +- examples/bts/12934/why3session.xml | 12 +- examples/einstein/why3session.xml | 26 +- examples/hello_proof/why3session.xml | 31 +- examples/my_cosine/why3session.xml | 23 +- .../why3session.xml | 13 +- .../programs/binary_search/why3session.xml | 13 +- examples/programs/bresenham/why3session.xml | 53 ++- .../checking_a_large_routine/why3session.xml | 38 +-- examples/programs/decrease1/why3session.xml | 149 +++++---- .../programs/edit_distance/why3session.xml | 223 +++++++------ examples/programs/euler001/why3session.xml | 57 ++-- examples/programs/fact/why3session.xml | 13 +- examples/programs/fib_memo/why3session.xml | 16 +- examples/programs/find/why3session.xml | 193 ++++++----- examples/programs/gcd/why3session.xml | 27 +- examples/programs/gcd_bezout/why3session.xml | 55 ++-- .../programs/insertion_sort/why3session.xml | 191 ++++++----- .../insertion_sort_list/why3session.xml | 47 ++- examples/programs/isqrt/why3session.xml | 119 ++++--- examples/programs/kmp/why3session.xml | 301 +++++++++--------- examples/programs/mccarthy/why3session.xml | 61 ++-- .../programs/mergesort_list/why3session.xml | 70 ++-- examples/programs/muller/why3session.xml | 67 ++-- examples/programs/my_cosine/why3session.xml | 29 +- examples/programs/power/why3session.xml | 79 +++-- examples/programs/queens/why3session.xml | 247 +++++++------- examples/programs/quicksort/why3session.xml | 139 ++++---- examples/programs/same_fringe/why3session.xml | 36 +-- .../programs/selection_sort/why3session.xml | 97 +++--- examples/programs/sf/why3session.xml | 82 ++--- examples/programs/sorted_list/why3session.xml | 15 +- .../tortoise_and_hare/why3session.xml | 25 +- .../programs/vstte10_aqueue/why3session.xml | 35 +- .../vstte10_inverting/why3session.xml | 104 +++--- .../programs/vstte10_max_sum/why3session.xml | 279 ++++++++-------- .../programs/vstte10_queens/why3session.xml | 45 ++- .../vstte10_search_list/why3session.xml | 131 ++++---- examples/programs/zeros/why3session.xml | 30 +- examples/regtests.sh | 14 +- .../scottish-private-club/why3session.xml | 18 +- src/ide/session.ml | 24 +- src/ide/termcode.ml | 62 ++++ src/ide/termcode.mli | 4 + 44 files changed, 1659 insertions(+), 1651 deletions(-) diff --git a/examples/bts/12475/why3session.xml b/examples/bts/12475/why3session.xml index 37c3d05bc..4853b1afc 100644 --- a/examples/bts/12475/why3session.xml +++ b/examples/bts/12475/why3session.xml @@ -2,28 +2,25 @@ - + - + - - - - + - + - + - + - + diff --git a/examples/bts/12934/why3session.xml b/examples/bts/12934/why3session.xml index 8e9843862..e435ff41b 100644 --- a/examples/bts/12934/why3session.xml +++ b/examples/bts/12934/why3session.xml @@ -1,11 +1,17 @@ - + + + + + + + - + - + diff --git a/examples/einstein/why3session.xml b/examples/einstein/why3session.xml index 43807ae9f..d7ccfd0af 100644 --- a/examples/einstein/why3session.xml +++ b/examples/einstein/why3session.xml @@ -1,6 +1,12 @@ - + + + + + + + @@ -9,28 +15,28 @@ - + - + - + - + - + - + - + - + - + diff --git a/examples/hello_proof/why3session.xml b/examples/hello_proof/why3session.xml index 047e896f6..eb385af39 100644 --- a/examples/hello_proof/why3session.xml +++ b/examples/hello_proof/why3session.xml @@ -1,45 +1,42 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/my_cosine/why3session.xml b/examples/my_cosine/why3session.xml index 8d3050215..2c8cc0f2a 100644 --- a/examples/my_cosine/why3session.xml +++ b/examples/my_cosine/why3session.xml @@ -2,34 +2,31 @@ - + - + - - - - + - + - + - + - + - + - + - + diff --git a/examples/programs/assigning_meanings_to_programs/why3session.xml b/examples/programs/assigning_meanings_to_programs/why3session.xml index 66188fc10..111c7b76b 100644 --- a/examples/programs/assigning_meanings_to_programs/why3session.xml +++ b/examples/programs/assigning_meanings_to_programs/why3session.xml @@ -2,26 +2,23 @@ - + - + - - - - + - + - + diff --git a/examples/programs/binary_search/why3session.xml b/examples/programs/binary_search/why3session.xml index 44f2aa22e..26429a652 100644 --- a/examples/programs/binary_search/why3session.xml +++ b/examples/programs/binary_search/why3session.xml @@ -2,22 +2,19 @@ - + - + - - - - + - + - + diff --git a/examples/programs/bresenham/why3session.xml b/examples/programs/bresenham/why3session.xml index f8741c475..85b65d2bf 100644 --- a/examples/programs/bresenham/why3session.xml +++ b/examples/programs/bresenham/why3session.xml @@ -2,78 +2,75 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/checking_a_large_routine/why3session.xml b/examples/programs/checking_a_large_routine/why3session.xml index ec3704a69..61ed4f21c 100644 --- a/examples/programs/checking_a_large_routine/why3session.xml +++ b/examples/programs/checking_a_large_routine/why3session.xml @@ -1,6 +1,6 @@ - + @@ -9,65 +9,65 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/decrease1/why3session.xml b/examples/programs/decrease1/why3session.xml index 313cfc842..4881cf6bb 100644 --- a/examples/programs/decrease1/why3session.xml +++ b/examples/programs/decrease1/why3session.xml @@ -1,223 +1,220 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/edit_distance/why3session.xml b/examples/programs/edit_distance/why3session.xml index 739cdf1dd..d6215c60e 100644 --- a/examples/programs/edit_distance/why3session.xml +++ b/examples/programs/edit_distance/why3session.xml @@ -2,305 +2,302 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/euler001/why3session.xml b/examples/programs/euler001/why3session.xml index f3826a5aa..052c20aa6 100644 --- a/examples/programs/euler001/why3session.xml +++ b/examples/programs/euler001/why3session.xml @@ -1,80 +1,77 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/fact/why3session.xml b/examples/programs/fact/why3session.xml index 9081349f9..deb13b322 100644 --- a/examples/programs/fact/why3session.xml +++ b/examples/programs/fact/why3session.xml @@ -2,26 +2,23 @@ - + - + - - - - + - + - + diff --git a/examples/programs/fib_memo/why3session.xml b/examples/programs/fib_memo/why3session.xml index e3ce33c7a..1329c28ec 100644 --- a/examples/programs/fib_memo/why3session.xml +++ b/examples/programs/fib_memo/why3session.xml @@ -9,26 +9,26 @@ - + - + - + - + - + - + - + - + diff --git a/examples/programs/find/why3session.xml b/examples/programs/find/why3session.xml index b5694258e..10be46f37 100644 --- a/examples/programs/find/why3session.xml +++ b/examples/programs/find/why3session.xml @@ -2,254 +2,251 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/gcd/why3session.xml b/examples/programs/gcd/why3session.xml index abc9e4cb2..14a62a5b7 100644 --- a/examples/programs/gcd/why3session.xml +++ b/examples/programs/gcd/why3session.xml @@ -2,41 +2,38 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/gcd_bezout/why3session.xml b/examples/programs/gcd_bezout/why3session.xml index 20cf2d1e9..4d7f4f7b1 100644 --- a/examples/programs/gcd_bezout/why3session.xml +++ b/examples/programs/gcd_bezout/why3session.xml @@ -2,76 +2,73 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/insertion_sort/why3session.xml b/examples/programs/insertion_sort/why3session.xml index 2e2697397..01da002b7 100644 --- a/examples/programs/insertion_sort/why3session.xml +++ b/examples/programs/insertion_sort/why3session.xml @@ -2,275 +2,272 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/insertion_sort_list/why3session.xml b/examples/programs/insertion_sort_list/why3session.xml index 4aba0b02d..990523937 100644 --- a/examples/programs/insertion_sort_list/why3session.xml +++ b/examples/programs/insertion_sort_list/why3session.xml @@ -2,69 +2,66 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/isqrt/why3session.xml b/examples/programs/isqrt/why3session.xml index 75a82b410..c85f0b507 100644 --- a/examples/programs/isqrt/why3session.xml +++ b/examples/programs/isqrt/why3session.xml @@ -1,176 +1,173 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/kmp/why3session.xml b/examples/programs/kmp/why3session.xml index 691f7dacd..ca99acdc2 100644 --- a/examples/programs/kmp/why3session.xml +++ b/examples/programs/kmp/why3session.xml @@ -2,412 +2,409 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/mccarthy/why3session.xml b/examples/programs/mccarthy/why3session.xml index d8c338941..d13919f24 100644 --- a/examples/programs/mccarthy/why3session.xml +++ b/examples/programs/mccarthy/why3session.xml @@ -2,96 +2,93 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/mergesort_list/why3session.xml b/examples/programs/mergesort_list/why3session.xml index 30f2ffcdb..81190e434 100644 --- a/examples/programs/mergesort_list/why3session.xml +++ b/examples/programs/mergesort_list/why3session.xml @@ -9,34 +9,34 @@ - + - + - + - + - + - + - + - + - + - + - + - + @@ -44,74 +44,74 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/muller/why3session.xml b/examples/programs/muller/why3session.xml index e6734f358..de5ba401b 100644 --- a/examples/programs/muller/why3session.xml +++ b/examples/programs/muller/why3session.xml @@ -2,101 +2,98 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/my_cosine/why3session.xml b/examples/programs/my_cosine/why3session.xml index 40f7192e6..61be3cbaa 100644 --- a/examples/programs/my_cosine/why3session.xml +++ b/examples/programs/my_cosine/why3session.xml @@ -2,41 +2,38 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/power/why3session.xml b/examples/programs/power/why3session.xml index 2bc4eb764..165a62a19 100644 --- a/examples/programs/power/why3session.xml +++ b/examples/programs/power/why3session.xml @@ -2,114 +2,111 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/queens/why3session.xml b/examples/programs/queens/why3session.xml index a88e522aa..62920e0e1 100644 --- a/examples/programs/queens/why3session.xml +++ b/examples/programs/queens/why3session.xml @@ -2,330 +2,327 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/quicksort/why3session.xml b/examples/programs/quicksort/why3session.xml index 8faf96bd4..1c666e351 100644 --- a/examples/programs/quicksort/why3session.xml +++ b/examples/programs/quicksort/why3session.xml @@ -2,198 +2,195 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/same_fringe/why3session.xml b/examples/programs/same_fringe/why3session.xml index 211f2a31f..2caade100 100644 --- a/examples/programs/same_fringe/why3session.xml +++ b/examples/programs/same_fringe/why3session.xml @@ -9,65 +9,65 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/selection_sort/why3session.xml b/examples/programs/selection_sort/why3session.xml index d4560b398..b7ed5766b 100644 --- a/examples/programs/selection_sort/why3session.xml +++ b/examples/programs/selection_sort/why3session.xml @@ -2,140 +2,137 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/sf/why3session.xml b/examples/programs/sf/why3session.xml index a1dc4472e..de7d746a6 100644 --- a/examples/programs/sf/why3session.xml +++ b/examples/programs/sf/why3session.xml @@ -9,121 +9,121 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/sorted_list/why3session.xml b/examples/programs/sorted_list/why3session.xml index 9bcd42890..48141077f 100644 --- a/examples/programs/sorted_list/why3session.xml +++ b/examples/programs/sorted_list/why3session.xml @@ -2,24 +2,21 @@ - + - + - - - - + - + - + - + diff --git a/examples/programs/tortoise_and_hare/why3session.xml b/examples/programs/tortoise_and_hare/why3session.xml index 8e67e6ba2..a5fd686a0 100644 --- a/examples/programs/tortoise_and_hare/why3session.xml +++ b/examples/programs/tortoise_and_hare/why3session.xml @@ -2,36 +2,33 @@ - + - + - - - - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_aqueue/why3session.xml b/examples/programs/vstte10_aqueue/why3session.xml index fc17d1a3a..87a00db48 100644 --- a/examples/programs/vstte10_aqueue/why3session.xml +++ b/examples/programs/vstte10_aqueue/why3session.xml @@ -2,53 +2,50 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_inverting/why3session.xml b/examples/programs/vstte10_inverting/why3session.xml index 41e923722..2e619a631 100644 --- a/examples/programs/vstte10_inverting/why3session.xml +++ b/examples/programs/vstte10_inverting/why3session.xml @@ -9,81 +9,81 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -92,76 +92,76 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_max_sum/why3session.xml b/examples/programs/vstte10_max_sum/why3session.xml index 91ae0bcfc..26f1366af 100644 --- a/examples/programs/vstte10_max_sum/why3session.xml +++ b/examples/programs/vstte10_max_sum/why3session.xml @@ -1,412 +1,409 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_queens/why3session.xml b/examples/programs/vstte10_queens/why3session.xml index 53919f66a..2e71fd278 100644 --- a/examples/programs/vstte10_queens/why3session.xml +++ b/examples/programs/vstte10_queens/why3session.xml @@ -2,64 +2,61 @@ - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/vstte10_search_list/why3session.xml b/examples/programs/vstte10_search_list/why3session.xml index f12c00d15..a071e6db8 100644 --- a/examples/programs/vstte10_search_list/why3session.xml +++ b/examples/programs/vstte10_search_list/why3session.xml @@ -1,191 +1,188 @@ - + - + - + - - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/programs/zeros/why3session.xml b/examples/programs/zeros/why3session.xml index b34b4523c..a8ac047f1 100644 --- a/examples/programs/zeros/why3session.xml +++ b/examples/programs/zeros/why3session.xml @@ -9,48 +9,48 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/regtests.sh b/examples/regtests.sh index 5f2bcbe8c..5cff4d81c 100755 --- a/examples/regtests.sh +++ b/examples/regtests.sh @@ -1,6 +1,18 @@ #!/bin/sh # regression tests for why3 +case "$1" in + "-force") + REPLAYOPT="-force" + ;; + "") + REPLAYOPT="" + ;; + *) + echo "$0: Unknown option '$1'" + exit 2 +esac + TMP=$PWD/why3regtests.out TMPERR=$PWD/why3regtests.err @@ -12,7 +24,7 @@ run_dir () { for f in `ls $1/*/why3session.xml`; do d=`dirname $f` echo -n "Replaying $d ... " - ../bin/why3replayer.opt $2 $d 2> $TMPERR > $TMP + ../bin/why3replayer.opt $REPLAYOPT $2 $d 2> $TMPERR > $TMP ret=$? if test "$ret" != "0" ; then echo -n "FAILED (ret code=$ret):" diff --git a/examples/scottish-private-club/why3session.xml b/examples/scottish-private-club/why3session.xml index d6168fcbe..caf459569 100644 --- a/examples/scottish-private-club/why3session.xml +++ b/examples/scottish-private-club/why3session.xml @@ -1,20 +1,26 @@ - + + + + + + + - + - + - + - + - + diff --git a/src/ide/session.ml b/src/ide/session.ml index 46bd4faaf..aed14a7f5 100644 --- a/src/ide/session.ml +++ b/src/ide/session.ml @@ -285,18 +285,18 @@ let save_status fmt s = | Done r -> save_result fmt r let save_proof_attempt fmt _key a = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" (prover_id a.prover) a.timelimit a.edited_as a.proof_obsolete; save_status fmt a.proof_state; fprintf fmt "@]@\n" let opt lab fmt = function | None -> () - | Some s -> fprintf fmt "%s=\"%s\" " lab s + | Some s -> fprintf fmt "%s=\"%s\"@ " lab s let rec save_goal fmt g = assert (g.goal_shape <> ""); - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" g.goal_name (opt "expl") g.goal_expl g.checksum g.proved g.goal_expanded g.goal_shape; Hashtbl.iter (save_proof_attempt fmt) g.external_proofs; @@ -304,25 +304,25 @@ let rec save_goal fmt g = fprintf fmt "@]@\n" and save_trans fmt _ t = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" t.transf.transformation_name t.transf_proved t.transf_expanded; List.iter (save_goal fmt) t.subgoals; fprintf fmt "@]@\n" let save_theory fmt t = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" t.theory_name t.verified t.theory_expanded; List.iter (save_goal fmt) t.goals; fprintf fmt "@]@\n" let save_file fmt f = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" f.file_name f.file_verified f.file_expanded; List.iter (save_theory fmt) f.theories; fprintf fmt "@]@\n" let save_prover fmt p = - fprintf fmt "@\n@[@]" + fprintf fmt "@\n@[@]" p.prover_id p.prover_name p.prover_version let save fname = @@ -330,7 +330,7 @@ let save fname = let fmt = formatter_of_out_channel ch in fprintf fmt "@\n"; fprintf fmt "@\n"; - fprintf fmt "@[" fname; + fprintf fmt "@[" fname; Util.Mstr.iter (fun _ d -> save_prover fmt d) (get_provers ()); List.iter (save_file fmt) (get_all_files()); fprintf fmt "@]@\n"; @@ -594,6 +594,7 @@ let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal = (* check sum *) (**********************) +(* let task_checksum t = (* TODO: ignore print_locs and print_labels flag *) (* even better: compute check_sum directly, similar to the shape *) @@ -610,6 +611,7 @@ let task_checksum t = eprintf "task %s, sum = %s@." tmp sum; *) sum +*) @@ -646,7 +648,7 @@ let raw_add_goal parent name expl sum shape topt exp = let key = O.create ~parent:parent_key () in let sum,shape = match topt with | None -> sum,shape - | Some t -> (task_checksum t, + | Some t -> (Termcode.task_checksum t, Termcode.t_shape_buf (Task.task_goal_fmla t)) in let goal = { goal_name = name; @@ -836,7 +838,7 @@ let associate_subgoals gname old_goals new_goals = (fun i g -> let id = (Task.task_goal g).Decl.pr_name in let goal_name = gname ^ "." ^ (string_of_int (i+1)) in - let sum = task_checksum g in + let sum = Termcode.task_checksum g in (i,id,goal_name,g,sum)) new_goals in @@ -1152,7 +1154,7 @@ let found_obsolete = ref false let reload_root_goal ~allow_obsolete mth tname old_goals t : goal = let id = (Task.task_goal t).Decl.pr_name in let gname = id.Ident.id_string in - let sum = task_checksum t in + let sum = Termcode.task_checksum t in let old_goal, goal_obsolete = try let old_goal = Util.Mstr.find gname old_goals in diff --git a/src/ide/termcode.ml b/src/ide/termcode.ml index f