[Agda] Bug reports

[Catarina Coquand]

Hello Olov,

even if we are not active at the sourceforge list it should be possible
to send error there because they should be forwarded to us. 

As you say there is a problem with the multiple updates, that I would
have to check all the code to understand.

The other problem that you adress, that it fills  in all meta-variables 
automatically
is how it supposed to work right now.  Before no automatic filling in of 
terms
where done if the user didn't want to, but now it does fill in 
everything becuase otherwise
hidden arguments doesn't work.

Maybe
one could go back to the old solution for visible arguments, but one has 
to think about
how it interacts with hidden args. So for now if you are not pleased 
with the automatic
solution you will have to change it by hand.

We have also experimented on filling in automatically generated terms 
with _
indicating that there is something here that can be automatically 
inferred, if
you want to experiment with that just replace the inferred term with _.

Regards

      Catarina


Olov Wilander wrote:

>
> Hello everyone,
>
> What's the right place for submitting bug reports nowadays?  The 
> sourceforge place looks rather sparsely populated (and doesn't have 
> the most recent cvs20041206 version either).
>
> I'm having a bit of trouble (using the 20041206 version):
>
>>> refinePrj "/home/olov/agdabug/hiddenbicat/E_functors.agda" 716 27 
>>> 126 D hom er ref
>>
> ---  ("tr#" 6) +++
> ---  ("updateReplace" (126 "(D.hom ? ?).er.ref"  (391 392))) +++
> ---  ("updateReplace" (392 "(F.objectfunction b)"  ())) +++
> ---  ("updateReplace" (391 "(G.objectfunction b)"  ())) +++
> ---  ("updateReplace" (391 "(G.objectfunction b)"  ())) +++
> ---  ("updateReplace" (392 "(F.objectfunction b)"  ())) +++
> ---  ("updateReplace" (392 "(F.objectfunction b)"  ())) +++
> ---  ("updateReplace" (391 "(G.objectfunction b)"  ())) +++
> ---  ("info" ("* Goals *" "")) +++
> ---  ("info" ("* Constraints *" "")) +++
>
> There's one obvious error -- the multiple updates -- but more 
> importantly, those updates probably shouldn't happen at all!  (I've 
> got local names for these things, and I'd prefer to use them 
> consistently.)  I can provide the offending code, if that would be 
> useful.
>
> Still, it's better than the 20041114 version, that'd give the same 
> number to both resulting `holes', causing some confusion in the emacs 
> interface....
>
> I'm currently also having a problem with structures -- a hidden 
> variable is a structure, and I'm given constraints for all fields of 
> the structure, fully specifying it, but the hidden variable is still 
> not considered solved.  Is there a simple reason for this?  This is 
> with the 20041114 version -- it might not be there with the December 
> verision, but I haven't got both accessible at the moment to check.
>
> I've got work-arounds, but they're not very pleasing....
>
> /olov
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda