Ali Caglayan
Ali Caglayan
Sometimes during development you may come across a Coq bug which you need to make an example for. My current workflow is to make a new file called bug.v and...
When writing Gallina code, it is very common to leave a hole for a yet to be filled term. Coq will provide an error saying that a hole could not...
Like we have hover for identifiers, it would be great to have hover for holes. OCaml already has something similar (maybe even a custom protocol). This would also tie in...
Here is the behavior we want: 1. Hover over a identifier which has an inductive type 2. Get a suggestion to destruct 3. Replace the identifier with a match statement...
This should allow greater composition with existing Coq nix setup. Importantly we should build coq-lsp with the same version of OCaml and findlib that the Coq derivation is using. WIP
After #378 we will have a status bar. For now we will only have an enabled/disabled icon for that button. We should consider other icons we might want to show...
This will allow for the github user not to show up in a projects insights. If you have a look at the project insights, you will see that the commits...
I've built and installed `fswatch` from sources on NetBSD and would like to give some feedback. It builds and installs fine. It would be nice if it could be packaged,...
ocamlfind generates a weird install instruction: ``` (install (progn (run %{make} install) (run install -m 0755 ocaml-stub %{bin}/ocaml))) ``` which installs over the ocaml installation. This is a no-no in...
Building Zarith fails with: ``` ocamlfind install -destdir "/home/ali/HoTT/outputs/out/lib/ocaml/4.14.1/site-lib/" zarith META zarith.cma libzarith.a z.cmi q.cmi big_int_Z.cmi zarith_top.cma z.mli zarith.cmxa zarith_version.cmx z.cmx q.cmx big_int_Z.cmx zarith.cmxs zarith.h q.mli big_int_Z.mli zarith.a z.cmti q.cmti...