search

leanprover-community / yasnippet-lean

3 stars 2 forks source link

add README with description #2

Open arademaker opened 5 years ago

arademaker commented 5 years ago

Hi, it would be nice to have a minimum description of the package. The gif image shared in the Zulip chat would help a lot.

cipher1024 commented 5 years ago

Good idea!

cipher1024 commented 5 years ago

I added a small one. What else would you like to see in to see in there?

arademaker commented 5 years ago

Hi @cipher1024 , for those like me not familiar with yasnippet, it would be good a point to the yasnippet essential documentation. The screenshot is helpful, but I can't see how/why the words changed to templates! ;-) You typed 'license' and the screen changed ... How?

Sorry, maybe this is a foolish question. But I didn't find in https://github.com/joaotavora/yasnippet how the templates are evoked.

arademaker commented 5 years ago

For configuration, I added (require 'yasnippet-lean) in my .emacs. Do I need anything else?

arademaker commented 5 years ago

Do I have to install yasnippet package itself?

arademaker commented 5 years ago

OK, I found that I need (yas-global-mode 1) too. It seems that some other command from lean-mode is conflicting with C-c C-s . When I type it, the error is that it can't find elan executable.

cipher1024 commented 5 years ago

If you disable yasnippet, does it fix things?

arademaker commented 5 years ago

Hum, evaluating (yas-global-mode 0) which I believe is disabling yesnippet, it doesn't fix it.

cipher1024 commented 5 years ago

So that's not an issue with yasnippet. Did you instead elan on your system? https://github.com/Kha/elan We can also move this discussion to Zulip and go back to yasnippet-lean specific issues

arademaker commented 5 years ago

Do I need elan to use yasnippet-lean mode?

cipher1024 commented 5 years ago

No it's just that C-c C-s is a lean-mode shortcut. You may have to remap manually that of yasnippet or suggest a new mapping for the yasnippet function that I can put in yasnippet-lean

cipher1024 commented 5 years ago

I see that lean-mode conflicts with yasnippet in one more way: C-c C-n gets us the next Lean error and a new yasnippet snippet. Maybe we should remap them to C-s C-s and C-s C-n (and remap C-c C-v also to C-s C-v for consistency)