Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CoqIDE on lablgtk3 #9279

Merged
merged 27 commits into from Mar 19, 2019

Conversation

@herbelin
Copy link
Member

commented Dec 23, 2018

Kind: feature

This is a version of CoqIDE building on top of lablgtk3. It still needs a development version of lablgtk3 for a minor change and otherwise would builds against the official beta3 version of lablgtk3 from @garrigue.

The following features are missing:

  • the possibility to add new keys for user queries
  • the possibility to add wizard tactics
  • the progression bar

I don't know if the two first features are commonly used. Personally, I never used them.

The deactivation of the progression bar is a bit frustrating. The pixmap would need to be redone with cairo (with an extra compilation dependency as far as I understand - cairo-ocaml or ocaml-cairo). Do we want to go in this direction? And if yes, I would probably need help. @ppedrot do you have a particular opinion?

Another minor loss is the stippling ("pointillé") of an incomplete Qed. To be honest, I had not noticed that the blue background was stippled. So, if I'm not the only one not to have noticed it, maybe it is not so critical. As far as I understood, it could be redone also using Cairo. What do you think (and especially @gares)?

Technically, it is unclear if we can make it for the next Debian freeze. In any case, @silene, @Zimmi48, depending on the schedule of 8.9, depending on what is possible with Debian, I'm ready to do a port of this PR on top of 8.8.2 and release an ad hoc version of 8.8 specifically for gtk3-based CoqIDE if this is the condition to have it in the next Debian stable.

  • Entry added in CHANGES.md.
  • Remove dead code in configwin*.ml if sure it will not be ported.
  • Remove temporary commit for building with lablgtk3.0.beta3 when 3.0.0 is out.
  • Use a discriminating color to replace stippling (used light sky blue)
  • Update windows build files

Fixes #7055.

@SkySkimmer

This comment has been minimized.

Copy link
Contributor

commented Dec 23, 2018

I guess you need to update the dependencies in the dockerfile and windows scripts.

@herbelin

This comment has been minimized.

Copy link
Member Author

commented Dec 23, 2018

I guess you need to update the dependencies in the dockerfile and windows scripts.

Is it dev/ci/docker/Dockerfile and dev/build/windows/? There is no opam package yet for lablgtk3 and the situation is changing fast. So, this shall have to be done in a later step. Putting a sticker in the meanwhile.

By the way, I made nothing for dune either (but I know that @ejgallego is following this closely, and, lablgtk3 may eventually have a dune-based building).

@jashug

This comment has been minimized.

Copy link
Contributor

commented Dec 23, 2018

I do all my Coq development in CoqIde. I haven't tried this new version (let me know if/when that would be helpful), but I can comment on the changes from the PR description:

  • I also have never used the first two missing features.
  • I found the progress bar a nice visual aid, and liked that you could click to move to a point within the file (to locate an axiom, for example). It is nice to have, but it's lack isn't a deal-breaker for me.
  • I found it useful that an incomplete Qed was styled differently, but am not attached to the stippling effect; I expect a solid light blue/grey background would work just as well for me.
@Zimmi48

This comment has been minimized.

Copy link
Member

commented Dec 23, 2018

Technically, it is unclear if we can make it for the next Debian freeze. In any case, @silene, @Zimmi48, depending on the schedule of 8.9, depending on what is possible with Debian, I'm ready to do a port of this PR on top of 8.8.2 and release an ad hoc version of 8.8 specifically for gtk3-based CoqIDE if this is the condition to have it in the next Debian stable.

I don't understand what you are hoping for / asking me exactly but Coq packages have always been completely outdated in Debian and there is no reason to hope that this would change. On the contrary, the best we can hope is that Debian maintainers actually remove the Coq package entirely so that there is no confusion anymore that Debian users should not install Coq using their distribution package manager, but prefer opam (or Nix) instead. Moreover, AFAICT the whole point of this PR was not so that we can have a Debian Coq package but so that CoqIDE continue to be buildable under Debian (otherwise, even with opam, it would have been a nightmare). If you are in contact with Debian maintainers, tell them it is important that opam 2.0 gets its way in before the freeze (maybe it's already the case, I have no idea). In any case, I am not fond of the idea of a new 8.8 release just for this.

Show resolved Hide resolved INSTALL
@Zimmi48

This comment has been minimized.

Copy link
Member

commented Dec 23, 2018

This is an example of situation where the flexibility that developing CoqIDE in its own repository would bring would overcome the cost: it could allow to do a new CoqIDE major release, depending on gtk3 and possibly compatible with all recently released versions of Coq...

coqide.opam Outdated
@@ -20,7 +20,7 @@ depends: [
"dune" { build & >= "1.4.0" }
"coqide-server"
"conf-gtksourceview"

This comment has been minimized.

Copy link
@SkySkimmer

SkySkimmer Dec 23, 2018

Contributor

Is this the right version?

This comment has been minimized.

Copy link
@herbelin

herbelin Dec 23, 2018

Author Member

I did not see an opam package for lablgtk3 yet. I guess that an opam package conf-gtksourceview3 or similar may have to be prepared at some time.

This comment has been minimized.

Copy link
@garrigue

garrigue Dec 23, 2018

There is one!
It is up to date with the released version, lablgtk-3.0.beta3.

This comment has been minimized.

Copy link
@garrigue

garrigue Dec 23, 2018

And there is a conf-gtksourceview3 too.

This comment has been minimized.

Copy link
@herbelin

herbelin Dec 23, 2018

Author Member

Ah, ok!

Then, I upgraded the opam file (anticipating on the release number 3.0.0).

let strings = Configwin_ihm.strings
let list = Configwin_ihm.list
*)

This comment has been minimized.

Copy link
@SkySkimmer

SkySkimmer Dec 23, 2018

Contributor

Why keep this commented?

This comment has been minimized.

Copy link
@herbelin

herbelin Dec 23, 2018

Author Member

If the outcome of the discussion is that the user query and wizard tactics preferences are not worth being preserved and/or that noone is motivated to adapt the code and use the recommanded tree_store feature in place of the current clist, I guess that the corresponding code, become dead, can indeed be removed completely.

Otherwise said, until there is some visibility on what this code will become, I preferred to keep it in the files at the current stage and to ask ourselves this question again before merging.

@@ -119,6 +120,7 @@ val list : ?editable: bool -> ?help: string ->
('a -> string list) ->
'a list ->
parameter_kind
*)

This comment has been minimized.

Copy link
@SkySkimmer

SkySkimmer Dec 23, 2018

Contributor

Why keep this commented?

@@ -279,10 +278,10 @@ class ['a] list_selection_box
(* initialize the clist with the listref *)
self#update !listref
end;;

*)

This comment has been minimized.

Copy link
@SkySkimmer

SkySkimmer Dec 23, 2018

Contributor

Why keep this commented? etc for any other commented blocks.

@herbelin herbelin force-pushed the herbelin:master+coqide-on-lablgtk3 branch from c0eed61 to 7ce5ac5 Dec 23, 2018

@herbelin

This comment has been minimized.

Copy link
Member Author

commented Dec 23, 2018

@Zimmi48: I feel rather powerless to answer your questions about Debian. I don't have a clear picture of how spread is Debian among Coq users nor how these Debian users install Coq. I don't have a clear picture of how important it is for Coq users in general to use the last version. I don't know how much opam or nix is used for installing.

I don't know why Coq is so outdated in Debian. If it is deliberate from Debian maintainers, it would be better to have a header on the Coq Debian page telling how to install Coq without Debian rather than giving the impression to Debian users that Coq is "dying" and to Coq users that Debian is "dying". Actually, Debian maintainers for OCaml have served for so long time that I would not be surprised if they say that they would be happy that a new team take over (and actually Ralf T. who is one of the maintainers, told me something like that). The coming freeze could be a good opportunity to upgrade testing at least to 8.8, if not to 8.9.

Yes, the ability to compile CoqIDE via gtk3 on the next Debian stable is already a, or even the, crucial step.

Note that opam 2.0.1 seems to be already in Debian testing.

About releasing CoqIDE separately, it seems actually that this is the case in Debian. So, maybe, [added: if ever, to start with, there is a Coq 8.8.2 Debian package, then] it is enough to have a package named, say, coqide-on-gtk3-8.8.2???

@herbelin

This comment has been minimized.

Copy link
Member Author

commented Dec 24, 2018

@jashug: Thanks for feedback.

I found it useful that an incomplete Qed was styled differently, but am not attached to the stippling effect; I expect a solid light blue/grey background would work just as well for me.

Maybe can I just add a new color configuration item for incomplete Qed, with default solid light blue or grey background?

A digression: I heard that black background are recommended for the eyes. Would it be worth to develop a default style conceived on top of a black background? (Not that I'm competent though)

@gares

This comment has been minimized.

Copy link
Member

commented Dec 24, 2018

Wrt QED any colour would do.

@gares

This comment has been minimized.

Copy link
Member

commented Dec 24, 2018

In Debian the source package coq generates many binary packages among which there is coqide.

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Dec 24, 2018

I don't know why Coq is so outdated in Debian. If it is deliberate from Debian maintainers, it would be better to have a header on the Coq Debian page telling how to install Coq without Debian

Even if it's not deliberate but is just a lack of commitment, this would be preferable. I don't get what makes Debian maintenance so hard. People managing other package managers are pretty capable of keeping up.

About releasing CoqIDE separately, it seems actually that this is the case in Debian.

Releasing separately and having separate packages are two different things. We can generate many packages from a single release. This is the case in Debian, but also in opam, and someday it will probably be the case as well in Nix. However, having separate release cycles cannot be done while keeping the source of CoqIDE in the Coq repository, because this means that the version of CoqIDE and Coq are tied up together. In particular, what I was talking about was to release a CoqIDE version that would be compatible with lablgtk3 and a range of Coq versions.

@herbelin herbelin force-pushed the herbelin:master+coqide-on-lablgtk3 branch from 7ce5ac5 to 81fe53d Dec 24, 2018

@herbelin herbelin requested a review from coq/ci-maintainers as a code owner Dec 24, 2018

@gares

This comment has been minimized.

Copy link
Member

commented Dec 24, 2018

On my side it is just lack of time, maintenance is not very hard. The deb package is in good shape, afaict (wrt recent policies). I think I should ask for removal unless someone steps up, but I did not ask Stephan, maybe he has à différent opinion.

@herbelin

This comment has been minimized.

Copy link
Member Author

commented Dec 24, 2018

Even if it's not deliberate but is just a lack of commitment, this would be preferable. I don't get what makes Debian maintenance so hard. People managing other package managers are pretty capable of keeping up.

Someone from Debian could tell more. Possible hypotheses which maybe are completely wrong are: 1) being a Debian maintainer is demanding and involves a high responsibility: there is continuous integration made on several platforms which you have to watch, you have to follow closely the bug trackers of the corresponding packages, etc. 2) when the ratio pleasure/duties goes too low, it is more difficult to be motivated, and this ratio tends to naturally decrease with routine 3) Debian is somehow now more an institution than a fresh innovative project and people liable to take over happen to be more interested for instance in Nix or opam.

In particular, what I was talking about was to release a CoqIDE version that would be compatible with lablgtk3 and a range of Coq versions.

Then, I'm not sure exactly how to do this with the current dependencies. For instance, there are currently 3 shared directories, lib, clib, protocol. At first view, we would have to versionize the files in protocol to know if a given coqide is compatible with a given coqtop (or coqidetop).

@herbelin herbelin force-pushed the herbelin:master+coqide-on-lablgtk3 branch 2 times, most recently from 0b64b07 to 2446e87 Dec 24, 2018

@herbelin

This comment has been minimized.

Copy link
Member Author

commented Dec 24, 2018

Sorry @gares, I did not have seen your message which was answering my speculations.

On my side it is just lack of time, maintenance is not very hard. (...) I think I should ask for removal unless someone steps up (...)

So, let's start from this assumption, i.e. that it is either finding someone to take over or removing the package. Then, how to decide?

What I have difficulties to evaluate is the importance of being present in Debian. In the absolute, if we except the question of lack of time, would it better for the "community" to be in or better not? It seems to me that the question of how to organize ourselves at the level of the community so that the "community" gets what it needs should only come afterwards. In particular, if it makes sense to be in, I'm pretty sure that we shall find someone in the community to take over.

herbelin and others added some commits Nov 19, 2018

CoqIDE: Using Grid instead of Table.
This is not mandatory for gtk+3 since it is deprecated from only gtk
3.4. This would be needed for gtk+4 though.
CoqIDE: Use modify_bg rather than modify_base to change background co…
…lor.

The effect of modify_base is told to be widget-dependent. It uses to
change the background with gtk2 but not with gtk3. So we use the more
explicit modify_bg.
CoqIDE: Ensure that contents of the pref window expands as much as po…
…ssible.

This was not needed in gtk2 but is needed with gtk3.
CoqIDE: Ensure that the main 3 windows do not shrink when w/o contents.
This was automatic in gtk2 (apparently because of the specification
not being granted). This is needed with gtk3.
[coqide] [ci] Update GTK toolchain to lablgtk3
- Update Docker images to install compatible version of lablgtk3
- We remove unnecesary variables from configure.
- We fix path detection of GTK libs in makefile

@vbgl vbgl force-pushed the herbelin:master+coqide-on-lablgtk3 branch from 47d4088 to cef009d Mar 19, 2019

@ejgallego

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

I’ll fix the conflict on default.nix.

Thanks @vbgl ; @ppedrot , of course this is hard to predict but I have a feeling that GTK3 will provide a better experience to people when compared to the ancient GTK2,

@ejgallego

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

CI is OK, failure is the typical async problem.

@ppedrot

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

Let's merge...

@ppedrot ppedrot merged commit cef009d into coq:master Mar 19, 2019

7 of 9 checks passed

GitLab CI pipeline Pipeline completed with errors on GitLab CI
Details
test-suite:base+async job_execution_timeout on GitLab CI
Details
Pull request checks Passed.
Details
coq.coq Build #20190319.3 succeeded
Details
coq.coq (Windows) Windows succeeded
Details
coq.coq (macOS) macOS succeeded
Details
doc:ml-api:odoc: ml-api artifact Link to ml-api build artifact.
Details
doc:refman: refman artifact Link to refman build artifact.
Details
doc:refman: stdlib artifact Link to stdlib build artifact.
Details

ppedrot added a commit that referenced this pull request Mar 19, 2019

Merge PR #9279: CoqIDE on lablgtk3
Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: garrigue
Ack-by: herbelin
@ppedrot

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

BTW I am willing to reimplement the progress bar, does anybody knows what needs to be done?

@ejgallego

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

@ppedrot AFAICT you need to do the same as before but using Cairo [https://github.com/Chris00/ocaml-cairo]

TTBOMK the Cairo API should allow you to do quite interesting, and even fancy, stuff.

Note that indeed you may find that the lablgtk3 beta may want some better cairo interaction, but now you can do a quite interesting build setup, as all 3 cairo-ocaml, lablgtk3 and coq use Dune, you can just symlink the two libs into a vendor dir and hack the 3 projects at the same time [even getting merlin integration, but well I know you don't use merlin]

@ejgallego

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

By the way congrats to all involved here this was very hard work.

@ppedrot

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

@ejgallego Am I right that there is no Cairo bindings for lablgtk3 yet? So that I have to write them down first? Links to the documentation are broken and peeking at the API using OCaml toplevel is no fun...

@ejgallego

This comment has been minimized.

Copy link
Member

commented Mar 19, 2019

I think there are bindings indeed added by @sacerdot , there is also documentation, anyways it is pretty easy to generate using dune build @doc. Also, peeking at the API using dune utop is pretty pleasant.

@sacerdot

This comment has been minimized.

Copy link

commented Mar 19, 2019

Hi @ppedrot ,
yes, I connected lablgtk3 with cairo and pango. You can see examples in lablgtk3/examples/{drawing,pango1,pango2,nd}.ml

Let me know if you have any question.

@ppedrot

This comment has been minimized.

Copy link
Member

commented Mar 20, 2019

Indeed thanks, I managed to hack a quick adaptation to Cairo, I'll submit a PR soon.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.