BUGS

************************************************************************
* THIS FILE IS OUTDATED. PLASE USE BUGZILLA FOR FILING NEW BUG REPORTS *
*           See http://bugzilla.metaprl.org/                           *
************************************************************************

Note - some non-critical bugs may be documented as TODO items.
(You need to have MetaPRL CVS account to be able to access the doc/private/TODO file.)

Note - some files have small bugs documented in their comments, these can be found
by rgrep'ing for the string "BUG".

DOCUMENTATION:

1.1) Documentation suggests to use mp and x.mp
while mpopt and mptop should be used instead.
Use Guide and Tutorial should mention the difference,
and suggest using mptop or mpopt. After that all examples should use mpopt.
1.1.1) In the mptop/mpopt vs mp discussion, the documentation should also mention readline
and give some pointers (info+man pages or readline homepage) to more information on customizing it.

1.2) Make system is not documented (see TODO 7.02 for more information).

1.3) (Created on 1999.11.11 by nogin)
Resources and resource annotations are not documented
1.3.1) The dT tactic section (doc/htmlman/system/mp-d-tactic.html) is not written.

1.4) (Created on 1999.11.11 by nogin)
MetaPRL Tutorial is very outdated.

EDITOR

2.1-2.4 are fixed

2.5) Display form mode generality is not working.

2.6) (Added 2000.02.21 by nogin)
When a list of subgoals is too big, displaying used to take a while. The current
workaround is to only display subgoals when there are <20 of them. We 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 certain 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.

2.7) (Fixed in OCaml)

2.8) (fixed)

2.9) Display form mechanism does not give a way to distinguish between parameters
     and meta-parameters. Because of that terms with meta-parameters will very
     often display wrong.

REWRITER

(3.1-3.6 - fixed)

3.7) Currently rewriter does not enforce building contractum to be against the same redex
the contractum was compiled against. Hopefully we never do this wrong, but we still
should enforce it.

3.8) SO contexts that are not a part of a sequent are currently never used and as a result
the corresponding rewriter code is undebugged.

3.9) (fixed)

3.10) (nogin) When the same variable appears twice in the same bvars list
(e.g., spread{p; x,x.x}), Nuprl upderstands it as y,x.x and MetaPRL - as x,y.x.
Nuprl's way is more natural and we should convert. I already wrote the new type
inference (only for spread) with Nuprl's understanding in mind.

(3.11-3.14) fixed

REFINER

(4.1-4.6 - fixed)

4.7) (nogin)
In Ocaml, string is a mutable data structure. In MetaPRL, we use strings everywhere (variable
names, opnames, etc) as if they were immutable. We need to
a) Make sure that nobody can cheat the system by starting to mute strings.
b) Let the compiler and GC know that we are not going to mute strings (which should allow
them to be more efficient).

4.8-4.10) (fixed)

See also BUGS #4.4

4.11) (fixed)

PARSER & FILTER

5.1-5.6) (fixed)

5.7) (2001.07.18 nogin) Currently .prla ASCII IO requires stack size
proportional to the file size. This means that we will have a stack overflow
if .prla file is too big (I already had to increase the stack size because of
that). We should try to rewrite that code in a tail-recusive way.

RULES & REWRITES

6.1-6.2) (fixed)

6.3) (Moved to Bugzilla)

6.4) Dependent product type is currently defined as a very dependent function type.
Unfortunatelly, we were not (yet) able to prove productElimination. We should
think whether it's true and if not, then define dprod differently.

(6.5-6.6 - fixed)

BUILD SYSTEM

7.1) Dependencies between .prla, .prlb, .cmiz, .cmoz, etc., are all messed up
Solution: have MetaPRL maintain a file in each directory
with the list of valid files.  Have only one of .prla, .prlb, or .cmoz file
present at any time.  These files should not be in CVS.

Better solution: keep only one .prl file, can contain either binary or
ASCII.  Make CVS check that file is in ASCII before a commit.

Another problem is that when .prla is removed from the repository and
after "cvs update" removes it from the working copy, the old .prlb
becomes active instead of being deleted.

P.S. It's possible that omake (with its MD5 checksums) would be able to help
with this problem.

7.2-7.3) (fixed)