/[mojave]/metaprl/BUGS
ViewVC logotype

Log of /metaprl/BUGS

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 2924 - (view) (download) (annotate) - [select for diffs]
Modified Fri Mar 17 09:35:28 2000 UTC (21 years, 3 months ago) by nogin
File length: 6567 byte(s)
Diff to previous 2911
Removed conflicts introduced by jyh


Revision 2911 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 24 01:42:53 2000 UTC (21 years, 3 months ago) by jyh
File length: 7773 byte(s)
Diff to previous 2900
Planning for update to .prla files.


Revision 2900 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 21 23:11:58 2000 UTC (21 years, 3 months ago) by nogin
File length: 6472 byte(s)
Diff to previous 2883
When a list of subgoals is too big, displaying used to take a while. I implemented a
workaround - to only display subgoals when there are <20 of them. We'll need to
find a better solution - in particular we should take into account subgoal sizes, not only
the number of subgoals.

It may be a good idea to implement a generic display-form mechanism to allow limiting
the number of lines a sertain term would occupy. On the other hand, such an approach
would only save the time to output the display form, but not the time to produce it.


Revision 2883 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 16 00:31:35 2000 UTC (21 years, 4 months ago) by nogin
File length: 5906 byte(s)
Diff to previous 2857
Enabled the "strict" rewriter mode.

In "strict" mode, <<lambda{x.'t}>> will only match terms where "t" does not contain
free occurences of "x" while <<lambda{x.'t['x]}>> will match any lambda expression.
In "relaxed" mode both redices will match any lambda expression.

This is done
1) To force rule authors to completely specify the binding structure
2) To allow rule authors to specify free variables restrictions easier

refiner/refiner/refine.ml, filter/boot/rewrite_boot.ml and theories/tactic/tactic_cache.ml
use the strict mode.

filter/base/filter_prog.ml uses relaxed mode for d.f. and compiles ml rewrites
using the strict mode

refiner/reflib/dform.ml, refiner/reflib/term_dtable.ml and refiner/reflib/term_match_table.ml
use the relaxed mode.

Please let me know if this change breaks something.


Revision 2857 - (view) (download) (annotate) - [select for diffs]
Modified Sun Nov 21 22:19:12 1999 UTC (21 years, 6 months ago) by nogin
File length: 6336 byte(s)
Diff to previous 2847
BUG 2.3 now includes:

Loading the same theory twice produces similar problems.

As a result, `load'ing a theory and then `cd'ing into it
(which attempts to load the theory again) does not quite work.
As a temporary workaround, the "load" function was removed from
toploop.


Revision 2847 - (view) (download) (annotate) - [select for diffs]
Modified Thu Nov 11 21:00:33 1999 UTC (21 years, 7 months ago) by nogin
File length: 6051 byte(s)
Diff to previous 2845
- Edited the autoT section a little
- Added an empty section on dT
- Added some problems with missing or outdated documentation to BUGS
- Added references to tactic descriptions to User Guide.


Revision 2845 - (view) (download) (annotate) - [select for diffs]
Modified Sat Nov 6 00:14:15 1999 UTC (21 years, 7 months ago) by nogin
File length: 5806 byte(s)
Diff to previous 2830
Another "small" thing that we should be more careful about when compiling rewrites.


Revision 2830 - (view) (download) (annotate) - [select for diffs]
Modified Wed Oct 27 05:41:35 1999 UTC (21 years, 7 months ago) by nogin
File length: 5482 byte(s)
Diff to previous 2818
More fixes

I have finished proof-reading the introduction and the user's guide and
I still have tutorial and system description left.


Revision 2818 - (view) (download) (annotate) - [select for diffs]
Modified Sat Oct 16 21:28:15 1999 UTC (21 years, 8 months ago) by nogin
File length: 5374 byte(s)
Diff to previous 2816
Updated the bug list:
- The bug (3.4) is fixed (see my previous commit).
- Added more information on several other bugs.


Revision 2816 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 8 22:38:35 1999 UTC (21 years, 8 months ago) by nogin
File length: 5007 byte(s)
Diff to previous 2814
- Updated several bug descriptions
- Numbered all bugs so that we can easier refer to them
- I suggest that we start all bug descriptions by
i.j) (Added on <date> by <login>. Confirmed on <date> by <login> ...)
So that we know how old the bug is and when was the last time we actually saw the bug.
This should help us to determine which bugs may be already gone and which bugs
are around too long and need to be finally fixed


Revision 2814 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 27 18:07:30 1999 UTC (21 years, 8 months ago) by kopylov
File length: 5565 byte(s)
Diff to previous 2810
The rule interactive bunionElimination in the theory itt_bunion is not correct.
(This is a result of non-understanding hidden hypothesis)


Revision 2810 - (view) (download) (annotate) - [select for diffs]
Modified Thu Sep 2 19:34:39 1999 UTC (21 years, 9 months ago) by jyh
File length: 5422 byte(s)
Diff to previous 2736
Added some new BUGS and things TODO.


Revision 2736 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 21 00:41:38 1999 UTC (22 years ago) by nogin
File length: 4701 byte(s)
Diff to previous 2725
In "strict" mode rewriter now should correctly restrict free variables
in sequent contexts.

I postponed testing of this code until "strig" flag would be fully implemented.


Revision 2725 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 17 22:39:51 1999 UTC (22 years ago) by nogin
File length: 4564 byte(s)
Diff to previous 2707
Added: reduceEta is too strong


Revision 2707 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 13 15:21:46 1999 UTC (22 years ago) by nogin
File length: 4518 byte(s)
Diff to previous 2706
- Documented the behaviour of several functions when variable lists
have repeated entries.
In particular: <<x,x.'x>> is understood as <<x,y.'x>> by alpha_equality.

- Made sure that this behaviour of Term_ds and Term_std is consistent
with the documentation.

- Documented a bug in alpha_equal_match


Revision 2706 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 13 02:34:07 1999 UTC (22 years ago) by nogin
File length: 4088 byte(s)
Diff to previous 2704
Small changes


Revision 2704 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 12 00:22:28 1999 UTC (22 years ago) by nogin
File length: 4178 byte(s)
Diff to previous 2703
More problems


Revision 2703 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 20:49:17 1999 UTC (22 years ago) by nogin
File length: 4087 byte(s)
Diff to previous 2701
Fixed the "repeated meta-parameter" rewriter problem.
However, I have not checked the level expressions code yet.


Revision 2701 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 03:31:51 1999 UTC (22 years ago) by nogin
File length: 4089 byte(s)
Diff to previous 2700
More rewriter bugs.


Revision 2700 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 02:28:03 1999 UTC (22 years ago) by nogin
File length: 3798 byte(s)
Diff to previous 2685
Documented some rewriter bugs.


Revision 2685 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 2 09:14:37 1999 UTC (22 years ago) by nogin
File length: 2828 byte(s)
Diff to previous 2683
- added a display form for Summary!meta_function. Still, things do not
always look right - take, for example itt_int theory, intElimination rule

- copied itt_list.cmoz to itt_list.prlb to eliminate
"rules nilFormation do not match" warning


Revision 2683 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 2 02:16:00 1999 UTC (22 years ago) by nogin
File length: 2966 byte(s)
Diff to previous 2674
Produce more meaningful error messges when parsing terms in toploop.

Before:
# <<x>>;;
chars 17-18: Pcaml.Qerror("", 0, _)
# chars 20-22: Stream.Error("illegal begin of toplevel phrase")
#
...
# <<x>>;;
chars 57-58: Pcaml.Qerror("", 0, _)
# chars 60-62: Stream.Error("illegal begin of toplevel phrase")
#

Now:
# <<x>>;;
chars 17-18: Failure("Shell_p4.mk_opname: no current package")
# chars 20-22: Stream.Error("illegal begin of toplevel phrase")
#
...
# <<x>>;;
chars 57-58: Failure("Package_info.mk_opname: summary not initialized")
# chars 60-62: Stream.Error("illegal begin of toplevel phrase")
#


Revision 2674 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 26 00:41:08 1999 UTC (22 years ago) by nogin
File length: 3251 byte(s)
Diff to previous 2673
I removed @ from the parameter syntax for meta-parameters. Now
[xxx:s] is parsed as a meta-string parameter (MString "xxx") and
["xxx":s] is parsed as a string parameter (Sting "xxx")

I also copied .cmoz files to .prlb files until I've reached a fixpoint.


Revision 2673 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 25 20:28:16 1999 UTC (22 years ago) by nogin
File length: 3296 byte(s)
Diff to previous 2665
.


Revision 2665 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 21 23:34:22 1999 UTC (22 years ago) by kopylov
File length: 3407 byte(s)
Diff to previous 2661
Added: cd theory;; load theory;; <<it>> produces an error


Revision 2661 - (view) (download) (annotate) - [select for diffs]
Modified Fri May 21 01:22:28 1999 UTC (22 years, 1 month ago) by nogin
File length: 2897 byte(s)
Diff to previous 2654
- 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 2654 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 16 21:05:14 1999 UTC (22 years, 1 month ago) by kopylov
File length: 2457 byte(s)
Diff to previous 2653
Added: loading two theories that both include the same theory produces unexpected results


Revision 2653 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 16 20:49:56 1999 UTC (22 years, 1 month ago) by nogin
File length: 1836 byte(s)
Diff to previous 2652
Added: MetaPRL toploop does not produce any meaningful parsing errors

Fixed spelling.


Revision 2652 - (view) (download) (annotate) - [select for diffs]
Added Thu May 13 23:18:29 1999 UTC (22 years, 1 month ago) by kopylov
File length: 1550 byte(s)
1) Added a bug list into BUGS

2) Changed the keywords:
axiom -> rule  (.mli files)
primrw -> prim_rw  (.ml files)
rwthm -> thm_rw  (.ml files)

3) Fixed the rule Itt_struct.hypSubstitution


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