Stream: Coq devs & plugin devs

Topic: Status of retroknowledge in module types

Hugo Herbelin (Aug 28 2021 at 09:20):

I wonder what to think about retroknowledge in module types. It is currently accepted in the syntax but silently dropped. Would there be a problem at allowing them in a module type? E.g. as in:

Module Type M. Primitive float := #float64_type. End M.
Declare Module N : M.
Check float. (* Currently fail *)

Paolo Giarrusso (Aug 28 2021 at 13:26):

no clue about retroknowledge but why should that succeed before importing N? This does:

Check N.float.
Import N.
Check float.

And it makes sense to me.

Hugo Herbelin (Aug 28 2021 at 13:41):

Oops, my example was indeed not showing what I wanted to show. Check float works (after the missing Import) but what I expected to highlight is that the retroknowledge had not been registered:

Module Type M. Primitive float := #float64_type. End M.
Declare Module Import N : M.
Check float. (* ok *)
Primitive sqrt := #float64_sqrt. (* anomaly *)

while

Primitive float := #float64_type.
Check float. (* ok *)
Primitive sqrt := #float64_sqrt. (* ok *)

as well as

Module Import M. Primitive float := #float64_type. End M.
Check float. (* ok *)
Primitive sqrt := #float64_sqrt. (* ok *)

work.
Note that I don't thing we should be afraid about the anomaly, this seems mostly to be a test missing to check that #float64_type has been previously registered (reported as #14814).

Last updated: Oct 13 2024 at 01:02 UTC