search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

Highlight assume/admit? #91

Closed parno closed 6 years ago

parno commented 6 years ago

Would it be possible to highlight (via enlarged/bold text or scary emoticons), uncommented calls to assume or admit? It might help avoid those situations where all of your proofs start going through super smoothly, only you later realize that you left in an admit while debugging earlier. Not that it's ever happened to me of course. Asking for a friend.

cpitclaudel commented 6 years ago

Good idea. "admit" et al should already be displayed in a different font, but I've just made that font customizable (M-x customize-face fstar-risky-face). Should we make it look scarier by default, too?

parno commented 6 years ago

Hmm, I just updated my fstar-mode, and assume seems to be about the same font as assert (maybe slightly more purple?). Before I upgraded, admit wasn't anything special, but I may have missed some intermediate updates to fstar-mode. Now it shows up as red. For my friend's sake, I'd be inclined to make the default a bit larger and scarier, but I -- I mean my friend -- can at least use the new config option. Thanks for adding it!

emacs

cpitclaudel commented 6 years ago

Good point, thanks. assume is a special case because of assume val …. How should that be highlighted?

beurdouche commented 6 years ago

I would treat assume the same way admit is. : )

cpitclaudel commented 6 years ago

OK, just pushed this:

image

beurdouche commented 6 years ago

Cool, the assume part from the assume val is not dangerous though, but if it is ok for everyone, keeping it that way is fine with me : )

cpitclaudel commented 6 years ago

Cool, the assume part from the assume val is not dangerous though,

I'm confused, didn't you mean the opposite when you wrote "I would treat assume the same way admit is."?

beurdouche commented 6 years ago

~My bad the sentence should have been "I would treat assume alone the same way admit is. : )" ~

cpitclaudel commented 6 years ago

Ah, OK. Why is assume val safe?

beurdouche commented 6 years ago

Well actually not that much, it is true. In most cases I use assume val for unimplemented functions or "external" functions, but it could be the wrong spec too. I didn't immediately realize because I always give a let and an admit for my admitted lemmas but because we can assume val a lemma or whatever, it can also be unsafe... Sleep deprevation, sorry ! :( As I said this is a great change, I am totally fine with it ! Thanks Clément ;)

parno commented 6 years ago

I agree that it's okay to default to highlighting assume val as well. If it's an assumption about the external world, then you're not likely to remove it, but highlighting it would help you or a future reader notice the assumptions you've added.

On a separate note, FWIW, I think I'm up-to-date (I have version 20180708.1438 of fstar-mode), but my display still looks the same as before. This is Aquamacs though. When I try it in Emacs, it looks like Clement's display above, so it must be an Aquamacs thing.

cpitclaudel commented 6 years ago

Great, thanks.

cpitclaudel commented 6 years ago

On a separate note, FWIW, I think I'm up-to-date (I have version 20180708.1438 of fstar-mode)

Try updating again (MELPA doesn't build immediately after code is committed) :)

parno commented 6 years ago

I pulled again, and now assume is showing up in the same scary color as admit, so I think we're in good shape 👍

cpitclaudel commented 6 years ago

Thanks!