search

RedPRL / cooltt

😎TT
http://www.redprl.org/
Apache License 2.0
219 stars 16 forks source link

🤫 Support silent holes, closing #86 #339

Closed favonia closed 2 years ago

favonia commented 2 years ago

Blocked by the following PRs/issues:

favonia commented 2 years ago

Is there any way to detect when you have left a silent hole? (like “5 remaining holes”)

Are you suggesting a way to count the holes? If so, should the counting include all holes (not just the silent ones)?

Regardless of how we count them, I feel this might belong to another PR. We would have to change the state monad.

favonia commented 2 years ago

Why is the CI not running for this PR, by the way?

jonsterling commented 2 years ago

@favonia I realize these are in principle separable features, but I think it is very dangerous to have silent holes that do not give any indication to the user that the development is incomplete. In redtt for instance, I believe there was some indication that the development was incomplete.

Anyway, I am not picky about how this is achieved, but I think we should not add silent holes without having some kind of indication.

favonia commented 2 years ago

Anyway, I am not picky about how this is achieved, but I think we should not add silent holes without having some kind of indication.

I have a question whose answer could speed up my coding significantly: is the problem field in RefineEnv the holes? And, I suppose it's enough to print out the size of that field? https://github.com/RedPRL/cooltt/blob/96e92686b16f7b8b15ece3c745265485b788e513/src/core/RefineEnv.ml#L27-L42

jonsterling commented 2 years ago

Anyway, I am not picky about how this is achieved, but I think we should not add silent holes without having some kind of indication.

I have a question whose answer could speed up my coding significantly: is the problem field in RefineEnv the holes? And, I suppose it's enough to print out the size of that field?

https://github.com/RedPRL/cooltt/blob/96e92686b16f7b8b15ece3c745265485b788e513/src/core/RefineEnv.ml#L27-L42

No, the problem field is more of a namespace for holes so you can see where some hole came from. I intended it for when elaborating pattern matching or something, but never got around to really using it in a useful way. (Wouldn't mind if someone wanted to delete it.)

favonia commented 2 years ago

No, the problem field is more of a namespace for holes so you can see where some hole came from. I intended it for when elaborating pattern matching or something, but never got around to really using it in a useful way. (Wouldn't mind if someone wanted to delete it.)

OMG this is so misleading LOL. Perhaps we should clean up this before importing Big Thoughts.