Opam file outdated / Inclusion in Coq Platform

MSoegtropIMC commented 2 years ago

@ecranceMERCE : I find your tactic quite useful and at the same time find it sad that it starts to bit rot before it really took off.

I would consider the following steps:

discuss with @gares if he thinks it should be in Coq CI or if he has some extended ELPI CI or if the use of Elpi is simple enough to be unlikely to cause compatibility issues
update the opam file, change it to a tag and publish it in the main opam repo (you can use the opam file below - note the editorial change to the license to make it SPDX compatible)
consider a request to add it to the Coq Platform - which means you express your intention to maintain it for the foreseeable future (see https://github.com/coq/platform/blob/main/charter.md)

Since your supplied opam file does not work with recent Coq / Elpi, I am using this one with relaxed version restrictions, which works fine with latest Coq Platform release (2022.04 - currently in publishing) and binds to your 1.0 tag:

opam-version: "2.0"
name: "coq-trakt"
maintainer: "Enzo Crance <enzo.crance@inria.fr>"
authors: [ "Enzo Crance" ]
license: "LGPL-3.0"
homepage: "https://github.com/ecranceMERCE/trakt"
bug-reports: "https://github.com/ecranceMERCE/trakt/issues"
dev-repo: "git+https://github.com/ecranceMERCE/trakt.git"
build: [ make ]
install: [ make "install" ]
depends: [
  "coq-elpi" {>= "1.11.1" & < "1.14~"}
  "coq" {>= "8.13~" & < "8.16~" }
]
tags: [ 
  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
  "category:Miscellaneous/Coq Extensions"
  "keyword:automation"
  "keyword:elpi"
  "logpath:Trakt"
]
synopsis: "A generic goal preprocessing tool for proof automation tactics in Coq"
description: """
Trakt is a Coq plugin that provides a new Coq tactic, trakt, for preprocessing goals before handing them to a proof automation tactic, as well as Coq commands to fill a knowledge database before calling the tactic.

Drawing inspiration from the zify tactic in the Coq standard library, it acts like a type-level funnel by casting all the possible values in the goal into a given target type. It can also express logic in Prop or bool according to the user's choice.

The translation is implemented in Coq-Elpi. It is certifying (it leaves no proof obligation), generic (the translation does not focus on a precise theory, it is determined by the parameters and user knowledge), and efficient (it tries to make sparse use of Coq conversion).
"""
url {
  src: "https://github.com/ecranceMERCE/trakt/archive/refs/tags/1.0.tar.gz"
  checksum: [
    "sha512=0a49a0e2db5f68a02929ef734234727cf459b8353e31e2b54ae6a90fbcaa481251a449742b308aabd1e6b2f5cbf3593f032030565689d80dbea8582641e1b4fc"
  ]
}

gares commented 2 years ago

I think there is some work to make a nix package out of this, so I will be able to test it in Coq-Elpi's CI (eventually) automatically.

ecranceMERCE commented 2 years ago

Hello. This sounds great. I am willing to help for this package to be available to the community, but I will not be available next week. I will check this when I come back. Thanks for the notification.

MSoegtropIMC commented 2 years ago

There is no urgency - it is more about the long term perspective.

CohenCyril commented 2 years ago

Someone made a nix package out of this already, so I can easily contribute a coq-nix-toolbox setup. Also may I suggest to move the project to coq-community? Or at least to reuse their template (I can do it alone or with you if you want).

MSoegtropIMC commented 2 years ago

@gares : is this sufficient to integrate it into ELPI's CI?

gares commented 2 years ago

Yes, but only if @CohenCyril commits to maintain that CI, since I don't know much about nix and every time I try myself I get lost by the lack of doc (when google does not know, I don't either).

ecranceMERCE commented 2 years ago

I made a new release (https://github.com/ecranceMERCE/trakt/releases/tag/1.1), updated the opam file and requested to add the package to the main opam repository (https://github.com/coq/opam-coq-archive/pull/2176). Let's see how it goes. I will look into CI stuff and joining Coq Platform / coq-community but I am not knowledgeable in this domain. Thanks for your advice and help for the opam file.

MSoegtropIMC commented 2 years ago

@ecranceMERCE : what would be missing for inclusion in Coq Platform is a request here:

https://github.com/coq/platform/issues

stating that you (as maintainer) want it to be added and are fine with Coq Platform charter

ecranceMERCE / trakt

Opam file outdated / Inclusion in Coq Platform #3