Bug#304017: numerix.cmxa and numerix.a not packaged

2005-04-10 Thread Julien PUYDT
Package: libnumerix-ocaml-dev Version: 0.19-5 Hi, my little pet project's opt build-target was broken by the recent package upgrade (transition to 3.08.3) because the two mentioned files are missing. Compiling the numerix source package and manually installing them solves my issue, so it

Re: Bug#246846: Is this bug still present in lablgtk2 2.4.0+2005.02.18-1 ?

2005-05-07 Thread Julien PUYDT
Sven Luther a écrit : Hello, I would like to know if this bug was still present in the current version of lablgtk2 in sarge ? I don't know if it's the release in sarge, but I just rechecked the ones I pointed as problematic with the current lablgtk2 in unstable, and on those the result is: *

Re: Bug#246846: Is this bug still present in lablgtk2 2.4.0+2005.02.18-1 ?

2005-05-08 Thread Julien PUYDT
Sven Luther a écrit : * csview.ml: File csview.ml, line 51, characters 4-6: Syntax error csview.ml uses stream parsers, which are provided by camlp4. There is now a comment in the file: (* Compile with ocamlc -pp camlp4o -I +lablgtk2 lablgtk.cma csview.ml -o csview or run with lablgtk2

Bug#514265: Broken link in the libbatteries-ocaml-doc

2009-02-05 Thread Julien PUYDT
Package: libbatteries-ocaml-doc Version: 0.20081112+gitBB342A7-1 The /usr/share/doc/libbatteries-ocaml-doc/examples/myocamlbuild.ml link is broken. Hope it helps, Snark on #ocaml -- To UNSUBSCRIBE, email to debian-ocaml-maint-requ...@lists.debian.org with a subject of unsubscribe.

Bug#515792: Missing build-dep on ocamlnet

2009-02-17 Thread Julien PUYDT
Package: ocaml-batteries-included Severity: low I was trying to apply the existing debian .diff.gz on the latest batteries sources (alpha3) to obtain more recent packages, but failed to build because ocamlnet wasn't installed -- although I had apt-get build-dep. Hope this helps, Snark on

Bug#883018: Please make ocaml-nox provide ocamlopt (or not) depending on arch

2017-11-28 Thread Julien Puydt
Package: ocaml-nox Version: 4.05.0-10 Severity: wishlist Hi, I just took the scilab package out of orphanage, and I'm having a problem : it has some caml code, but wants to compile it with ocamlopt, which is not available on all architectures. If you look at:

Bug#993045: Please bring back the -unsafe-string switch

2021-08-26 Thread Julien Puydt
Package: ocaml Version: 4.11.1-4 a part of scilab (modelica) is written in OCaml, but needs the -unsafe- string switch ; unfortunately: /usr/bin/ocaml: OCaml has been configured with -force-safe-string: - unsafe-string is not available. Can you please re-enable unsafe strings? Thanks, J.Puydt

Policy and packaging coq theories

2021-08-31 Thread Julien Puydt
Hi, I wanted to have a look at how the team works (mathcomp will need hierarchy-builder and coq-elpy, so perhaps some I could lend a hand). But on this page: https://wiki.debian.org/Teams/OCamlTaskForce a few links are dead (notably the policy, which I'll have to read from the dh-ocaml

Bug#993045: Please bring back the -unsafe-string switch

2021-09-07 Thread Julien Puydt
Le mardi 07 septembre 2021 à 13:30 +0200, Stéphane Glondu a écrit : > Le 06/09/2021 à 11:01, Julien Puydt a écrit : > > The configure script checks for the availability of the switch, and > > adds it to OCAMLCFLAGS... I checked String.set doesn't seem to be > > used > >

Bug#993045: Please bring back the -unsafe-string switch

2021-09-06 Thread Julien Puydt
Le lundi 06 septembre 2021 à 10:44 +0200, Stéphane Glondu a écrit : > Le 06/09/2021 à 10:08, Julien Puydt a écrit : > > > How come this is an issue only now? The transition to OCaml > > > 4.11.1 > > > (the > > > first version with unsafe strings

Bug#993045: Please bring back the -unsafe-string switch

2021-09-06 Thread Julien Puydt
Hi Le dimanche 29 août 2021 à 14:14 +0200, Stéphane Glondu a écrit : > Control: tags 993045 + wontfix > > Le 26/08/2021 à 21:42, Julien Puydt a écrit : > > a part of scilab (modelica) is written in OCaml, but needs the - > > unsafe- > > string switch ; unfortunate

Bug#1000954: Detect all clashing exported units at once

2021-12-01 Thread Julien Puydt
Package: dh-ocaml Version: 1.1.3 Severity: wishlist While trying to package coq-elpi, dh_ocaml found it exported units already exported by other packages ; so far so good. But it reports only the first one, not the whole list, so I would like Cheers, J.Puydt PS: example of error message: E:

Re: Trouble packaging coq-elpi

2021-12-01 Thread Julien Puydt
Hi, I could finally find some time for some digging. Le mardi 23 novembre 2021 à 10:13 +0100, Stéphane Glondu a écrit : > Le 22/11/2021 à 10:45, Julien Puydt a écrit : > > I'm trying to package coq-elpi (after I packaged elpi [in NEW], and > > before I can package hi

Building clean packages for coq theories

2021-11-18 Thread Julien Puydt
Hi, I updated src:coq, I uploaded src:elpi (to NEW). I'm trying to create a nice package for coq-elpi, but I'm not sure exactly how to do that. The examples I have are coq's standard library and ssreflect. And neither looks clean. By this I mean that for coq, there's coq-theories, and it ships

Bug#999483: ITP: coq-elpi -- Coq plugin embedding Elpi

2021-11-11 Thread Julien Puydt
Package: wnpp Owner: Julien Puydt X-Debbugs-CC: debian-ocaml-maint@lists.debian.org Severity: wishlist * Package name: coq-elpi Version : 1.11.2 Upstream Author : Enrico Tassi * URL : https://github.com/LPCIC/coq-elpi * License : LGPL 2.1+ Programming Lang

On packaging coq plugins

2021-11-11 Thread Julien Puydt
Hi, I'm starting to package my first Coq plugin, so I'm a bit unsure how to proceed: there doesn't seem to be that many examples. There are two libraries (src:coq-float and src:ssreflect) -- but they provide coq theories, so they look like coq-theories (from src:coq): a big number of .v, .vo,

Re: Lintian warnings with the coq package

2021-11-11 Thread Julien Puydt
tem /bin/bash, not /usr/bin/bash. Anyway, either bash > should be replaced by /bin/sh, or we need a build-dependency on bash. > I saw the build was broken on a few architectures but didn't investigate yet ; indeed I'll try get rid of that use of bash. On Wed, Nov 10, 2021 at 11:40:37AM +0100,

Lintian warnings with the coq package

2021-11-10 Thread Julien Puydt
Hi, I'm still not satisfied with the coq package I prepared : lintian finds too much to complain about. PROBLEM I: shared-library-lacks-prerequisites lintian warnings (many of them) For example: W: libcoq-ocaml: shared-library-lacks-prerequisites usr/lib/coq- core/clib/clib.cmxs My

Bug#999602: [false positive] shared-library-lacks-prerequisites

2021-11-13 Thread Julien Puydt
Package: lintian Version: 2.111.0 X-Debbugs-CC: debian-ocaml-maint@lists.debian.org The Coq project comes with a kind of compiler, and generates files that are ELF shared objects ; as such they do get detected by lintian, and it tries to analyse them just like normal C/C++ shared objects.

Bug#999601: [false positive] ocaml-dangling-cmi hint needs refinement

2021-11-13 Thread Julien Puydt
Package: lintian Version: 2.111.0 X-Debbugs-CC: debian-ocaml-maint@lists.debian.org A new build system is seeing increasing use in the OCaml world, and is putting the above hint implementation out of its depth: dune. The current implementation of the hint is that for each foo.cmi, there should

Re: Architectures supported by the coq package

2021-11-24 Thread Julien Puydt
Hi, Le mercredi 24 novembre 2021 à 08:23 +0100, Stéphane Glondu a écrit : > > I've seen you've restricted the Architectures list of the coq > package. > Is this a temporary measure? Or is Coq definitely dropping support > for bytecode architectures? It's just a temporary measure ; I hope we'll

Re: Building clean packages for coq theories

2021-11-24 Thread Julien Puydt
Le mardi 23 novembre 2021 à 10:09 +0100, Stéphane Glondu a écrit : > > META is usually put in libfoobar-ocaml, as it contains the > information to locate the *.cma and *.cmxs files (this information is > used by anything using findlib as a lib, for example ocsigenserver). Indeed, that's what's

Bug#1000573: Bytecode architectures blocking bug

2021-11-25 Thread Julien Puydt
Package: coq Version: 8.14.0+dfsg-6 Severity: grave X-Debbugs-CC: debian-ocaml-maint@lists.debian.org Don't migrate to testing until the bytecode architectures' situation is cleared. Cheers, J. Puydt

Trouble packaging coq-elpi

2021-11-22 Thread Julien Puydt
Hi, I'm trying to package coq-elpi (after I packaged elpi [in NEW], and before I can package hierarchy-builder), but dh_ocaml gives me an error and I don't get it: E: Error: unit Extfun exported in libcoq-elpi-ocaml-dev/libcoq-elpi- ocaml v1.11.2-1 but already exported by camlp5 v7.14-1 But

Re: Building clean packages for coq theories

2021-11-22 Thread Julien Puydt
Hi, Le lundi 22 novembre 2021 à 09:01 +0100, Ralf Treinen a écrit : > > On Fri, Nov 19, 2021 at 08:04:44AM +0100, Julien Puydt wrote: > > > And for ssreflect, it ships a single libssreflect-coq package ; > > it's > > shipping .v, .vo and .glob files and the html doc.

Bug#999651: marked as pending in coq

2021-11-14 Thread Julien Puydt
Control: tag -1 pending Hello, Bug #999651 in coq reported by you has been fixed in the Git repository and is awaiting an upload. You can see the commit message below and you can check the diff of the fix at:

Bug#998291: ITP: ocaml-ansi-terminal -- colors and cursor movements for OCaml applications

2021-11-01 Thread Julien Puydt
Package: wnpp Owner: Julien Puydt X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Severity: wishlist * Package name: ocaml-ansi-terminal Version : 0.8.2 Upstream Author : Christophe Troestler & Vincent Hugot * URL : https://github.com/Chris00/ANSITerminal * Lic

Updating coq

2021-11-02 Thread Julien Puydt
Hi, I tried to have a look at the coq package (I need a newer version for coq-elpi), and didn't quite get how to do that: - debian/copyright says the source have to be edited, but doesn't say how ; - debian/README.source says gbp.conf does the trick and the version name should have a +dfsg

Packaging elpi, hierarchy-builder and recent a mathcomp -- starting to work on it

2021-10-27 Thread Julien Puydt
Hi, as I wrote to this list in august, I'm interested in coq theories, and specifically mathcomp, which will soon require hierarchy-builder, wich requires coq-elpi, which requires elpi. I am a Debian developer and I am already part of a few teams (games, javascript, python and science), so I

Bug#997993: ITP: elpi -- embeddable lambda-Prolog interpreter

2021-10-28 Thread Julien Puydt
Package: wnpp Owner: Julien Puydt X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Severity: wishlist * Package name: elpi Version : 1.13.7 Upstream Author : Claudio Sacerdoti Coen and Enrico Tassi * URL : https://github.com/LPCIC/elpi * License : LGPL 2.1

Re: Packaging elpi, hierarchy-builder and recent a mathcomp -- starting to work on it

2021-10-28 Thread Julien Puydt
Hi, Le jeudi 28 octobre 2021 à 09:24 +0200, Stéphane Glondu a écrit : > > Le 27/10/2021 à 18:40, Julien Puydt a écrit : > > as I wrote to this list in august, I'm interested in coq theories, > > and > > specifically mathcomp, which will soon require hierarchy-builder, &

Re: Packaging elpi, hierarchy-builder and recent a mathcomp -- starting to work on it

2021-10-29 Thread Julien Puydt
Le jeudi 28 octobre 2021 à 09:24 +0200, Stéphane Glondu a écrit : > > Feel free to push your git repository there. > Access request still pending. I improved my elpi package, see https://mentors.debian.net/packages/elpi/ I'm wondering why "ocamlfind list" shows its version as n/a. The next

Re: Updating coq

2021-11-08 Thread Julien Puydt
Hi, Le mercredi 03 novembre 2021 à 09:03 +0100, Ralf Treinen a écrit : > > good to hear that you are joining the team and that you are interested > in coq and related packages. The coq package is (again) lacking behind > upstream, so we could definitely use some help here. I had uopdated the >

Re: Bug#1001493: RM: coq [alpha armel hppa ia64 m68k mips64el mipsel sh4 sparc64 x32] -- RoM ; abandoned upstream

2021-12-13 Thread Julien Puydt
Hi, Le samedi 11 décembre 2021 à 17:38 -0500, Scott Kitterman a écrit : > On Fri, 10 Dec 2021 22:59:57 +0100 Julien Puydt > > wrote: > > Package: ftp.debian.org > > Usertags: rm > > X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org > > > > Upstream decide

Bug#1001493: RM: coq [alpha armel hppa ia64 m68k mips64el mipsel sh4 sparc64 x32] -- RoM ; abandoned upstream

2021-12-10 Thread Julien Puydt
Package: ftp.debian.org Usertags: rm X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Upstream decided those architectures weren't supported anymore ; I removed support for them from my last upload, but they still have old binary packages lying around in the unstable archive, and those should

Bug#1003438: RM: why3 [alpha armel hppa ia64 m68k mipsel64el mipsel sh4 sparc64 x32] -- broken by missing coq

2022-01-09 Thread Julien Puydt
Package: ftp.debian.org Usertags: rm X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Since coq upstream abandoned some architecture, coq isn't available anymore on those architectures, and lingering binary packages prevent testing migration. Apparently the coq binary packages can't be removed

Bug#1003434: RM: prooftree [alpha armel hppa ia64 m68k mipsel64el mipsel sh4 sparc64 x32] -- broken by missing coq

2022-01-09 Thread Julien Puydt
Package: ftp.debian.org Usertags: rm X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Since coq upstream abandoned some architecture, coq isn't available anymore on those architectures, and lingering binary packages prevent testing migration. Apparently the coq binary packages can't be removed

Bug#1003435: RM: ssreflect [alpha armel hppa ia64 m68k mipsel64el mipsel sh4 sparc64 x32] -- broken by missing coq

2022-01-09 Thread Julien Puydt
Package: ftp.debian.org Usertags: rm X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Since coq upstream abandoned some architecture, coq isn't available anymore on those architectures, and lingering binary packages prevent testing migration. Apparently the coq binary packages can't be removed

Bug#1003436: RM: aac-tactics [alpha armel hppa ia64 m68k mipsel64el mipsel sh4 sparc64 x32] -- broken by missing coq

2022-01-09 Thread Julien Puydt
Package: ftp.debian.org Usertags: rm X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Since coq upstream abandoned some architecture, coq isn't available anymore on those architectures, and lingering binary packages prevent testing migration. Apparently the coq binary packages can't be removed

Bug#1003437: RM: coq-float [alpha armel hppa ia64 m68k mipsel64el mipsel sh4 sparc64 x32] -- broken by missing coq

2022-01-09 Thread Julien Puydt
Package: ftp.debian.org Usertags: rm X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Since coq upstream abandoned some architecture, coq isn't available anymore on those architectures, and lingering binary packages prevent testing migration. Apparently the coq binary packages can't be removed

Re: Bug#1003438: RM: why3 [alpha armel hppa ia64 m68k mipsel64el mipsel sh4 sparc64 x32] -- broken by missing coq

2022-01-10 Thread Julien Puydt
Hi Le mar. 11 janv. 2022 à 08:15, Ralf Treinen a écrit : > On Mon, Jan 10, 2022 at 08:39:25AM +0100, Julien Puydt wrote: > > Package: ftp.debian.org > > Usertags: rm > > X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org > > > > Since coq upstream abandoned some

Bug#1003586: Fixed in next upstream

2022-01-17 Thread Julien Puydt
Hi, I checked that next upstream (currently at RC1 stage) has a fix for that ; depending on the schedule of that next upstream, I'll either adapt the patch for us or wait for it. Cheers, J.Puydt

Bug#1003586: marked as pending in coq

2022-01-17 Thread Julien Puydt
Control: tag -1 pending Hello, Bug #1003586 in coq reported by you has been fixed in the Git repository and is awaiting an upload. You can see the commit message below and you can check the diff of the fix at:

Re: Updating menhir

2022-03-18 Thread julien . puydt
Hi, Le vendredi 18 mars 2022 à 08:43 +0100, Ralf Treinen a écrit : > On Thu, Mar 17, 2022 at 05:20:58PM +0100, > julien.pu...@gmail.com wrote: > > > I didn't upload it because the reverse deps situation wasn't > > perfect: > > Can you upload to experimental, please ? -Ralf. I never think about

Re: Updating menhir

2022-03-18 Thread julien . puydt
Hi, Le vendredi 18 mars 2022 à 08:21 +0100, Stéphane Glondu a écrit : > Le 17/03/2022 à 17:20, julien.pu...@gmail.com a écrit : > > I updated menhir on salsa to the last upstream -- and in the > > process, > > it got a +ds suffix because I kicked the prebuilt documentation out > menhir is a

Re: [why3] dropping coq support ?

2022-03-18 Thread julien . puydt
Hi, Le lundi 14 mars 2022 à 19:50 +0100, Ralf Treinen a écrit : > > Do others on this list have any thoughts about that? There are several points to take into account: (1) I dropped support for some architectures in the Debian package for coq, until upstream fixes them:

Bug#1005920: closed by Debian FTP Masters (reply to Julien Puydt ) (Bug#1005920: fixed in coq-doc 8.15.0-3)

2022-02-24 Thread Julien Puydt
Le mercredi 23 février 2022 à 13:21 +0100, Andreas Beckmann a écrit : > With all these B-D added, the build fails for me now with > > Running[3870]: (cd _build/default/doc && /usr/bin/env sphinx-build -q > -W -b html sphinx refman-html) > Command [3870] exited with code 2: > $ (cd

Bug#1005920: closed by Debian FTP Masters (reply to Julien Puydt ) (Bug#1005920: fixed in coq-doc 8.15.0-3)

2022-02-24 Thread Julien Puydt
Hi, Le mercredi 23 février 2022 à 13:21 +0100, Andreas Beckmann a écrit : > With all these B-D added, the build fails for me now with > > Not sure what exactly causes the failure ... It's an heisenbug: - I added a patch to get more log ; - I tried to build the package: success ; - I tried

Bug#970453: coq-float looks dead upstream: RM?

2022-02-19 Thread Julien Puydt
Hi, I was looking around at all coq-related packages and found this poor thing, which seems pretty dead. I propose to ask for its removal ; I'll proceed in a few weeks if nobody objects. Cheers, J.Puydt

On the coq ecosystem in Debian

2022-03-24 Thread julien . puydt
Hi, I'm trying to get more of the coq ecosystem into Debian. There are several things I would like to package -- but first I think I need to consolidate what's already there. Here is a list of issues I have, on which I would need feedback ; I put explicit "Question: ..." to make it clearer what

Re: On the coq ecosystem in Debian

2022-04-04 Thread julien . puydt
Hi, Le mardi 29 mars 2022 à 23:23 +0200, Ralf Treinen a écrit : > Hello, > > On Tue, Mar 29, 2022 at 09:52:16AM +0200, > julien.pu...@gmail.com wrote: > > Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit : > > > > > Question: shouldn't I split the current libcoq-elpi in a > > > >

Re: On the coq ecosystem in Debian

2022-03-29 Thread julien . puydt
Hi, Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit : > Le 24/03/2022 à 21:59, julien.pu...@gmail.com a écrit : > > Question: how are such things done? (pointers to code and/or > > documentation are welcome) > > I am not aware of a consolidated documentation for that :-( I will >

Re: On the coq ecosystem in Debian

2022-03-29 Thread julien . puydt
Le lundi 28 mars 2022 à 08:14 +0200, Stéphane Glondu a écrit : > Le 24/03/2022 à 21:59, julien.pu...@gmail.com a écrit : > > Question: shouldn't I split the current libcoq-elpi in a libcoq- > > elpi > > for the purely coq part and a libcoq-elpi-ocaml packages for the > > .cma/.cmxs pair? > > This

Coq-based packages

2022-02-04 Thread Julien Puydt
Hi, I just changed the binary packages provided by the source coq package to follow more closely upstream's subpackages. I used Provides+Breaks+Replaces so things should go smoothly. Now I would like to work on other things: (1) the source package coq-doc (non-free) should be updated to latest

Bug#1005214: ITP: mathcomp-finmap -- finite sets and maps extension for Mathematical Components

2022-02-08 Thread Julien Puydt
Package: wnpp X-Debbugs-Cc: debian-de...@lists.debian.org Owner: Julien Puydt X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Severity: wishlist * Package name: mathcomp-finmap Version : 1.5.1 Upstream Author : Cyril Cohen * URL : https://github.com/math-comp/finmap

Bug#1005215: ITP: mathcomp-bigenough -- epsilon - N reasoning for Mathematical Components

2022-02-08 Thread Julien Puydt
Package: wnpp X-Debbugs-Cc: debian-de...@lists.debian.org Owner: Julien Puydt X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Severity: wishlist * Package name: mathcomp-bigenough Version : 1.5.1 Upstream Author : Cyril Cohen * URL : https://github.com/math-comp

Bug#1005224: ITP: mathcomp-analysis -- analysis extension for Mathematical Components

2022-02-09 Thread Julien Puydt
Package: wnpp X-Debbugs-Cc: debian-de...@lists.debian.org Owner: Julien Puydt X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org Severity: wishlist * Package name: mathcomp-analysis Version : 0.3.13 Upstream Author : Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling

Bug#1002988: Too early to fix

2022-01-19 Thread Julien Puydt
Hi, upstream didn't release a new version with support for camlp5 8.* ; but they have a patch here: https://github.com/LPCIC/elpi/pull/110/commits/f58341831b56ccfe5f2f49158c600e4e36bcb9b5 so I should be able to fix the problem as soon as it actually occurs. Cheers, J.Puydt

Bug#1002988: Waiting for b-deps

2022-01-20 Thread Julien Puydt
Hi, now camlp5 8.* is in unstable the problem occurs ; I'm just waiting for the other b-deps to be available, but I have a commit ready. Cheers, J.Puydt

Re: Updating menhir

2022-04-07 Thread julien . puydt
Le vendredi 18 mars 2022 à 08:43 +0100, Ralf Treinen a écrit : > On Thu, Mar 17, 2022 at 05:20:58PM +0100, > julien.pu...@gmail.com wrote: > > > I didn't upload it because the reverse deps situation wasn't > > perfect: > > Can you upload to experimental, please ? -Ralf. > I found I needed the

Bug#1009116: ITP: pstm2-frontend -- Parse and type-check SMT-LIB 2

2022-04-07 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers * Package name: pstm2-frontend Version : 0.4.0 Upstream Author : Albin Coquereau * URL : https://github.com/ACoquereau/psmt2-frontend * License : Apache-2

Re: Next OCaml transition: 4.14.x

2023-09-18 Thread julien . puydt
Le lundi 18 septembre 2023 à 10:32 +0200, Stéphane Glondu a écrit : > Le 18/09/2023 à 10:04, Julien Puydt a écrit : > > I agree with that plan ; can you list which packages get broken in > > each > > case? > > I've attached the lists of (OPAM) packages that cannot

Re: Next OCaml transition: 4.14.x

2023-09-18 Thread Julien Puydt
Hi Le lun. 18 sept. 2023, 09:37, Stéphane Glondu a écrit : > > OCaml 5.1.0 has just been released, and a version 4.14.2 will soon be > released. Current version in unstable is 4.13.1. > > I played a bit with opam-debian-switch, and it turns out that (at least) > 35 packages are broken (at the

Bug#1050027: closed by Debian FTP Masters (reply to Julien Puydt ) (Bug#1050027: fixed in mathcomp-analysis 0.6.4-2)

2023-08-19 Thread julien . puydt
Le samedi 19 août 2023 à 20:58 +0200, Helmut Grohne a écrit : > Control: reopen -1 > Control: found -1 mathcomp-analysis/0.6.4-2 > > On Sat, Aug 19, 2023 at 05:33:11PM +, Debian Bug Tracking System > wrote: > > It has been closed by Debian FTP Masters > &

Bug#1044637: marked as pending in coq

2023-08-19 Thread Julien Puydt
Control: tag -1 pending Hello, Bug #1044637 in coq reported by you has been fixed in the Git repository and is awaiting an upload. You can see the commit message below and you can check the diff of the fix at:

Bug#1050027: libcoq-mathcomp-classical: undeclared file conflict with libcoq-mathcomp-analysis/bookworm+trixie

2023-08-23 Thread julien . puydt
Le mercredi 23 août 2023 à 09:07 +0100, Simon McVittie a écrit : > On Wed, 23 Aug 2023 at 08:41:44 +0200, julien.pu...@gmail.com wrote: > > let's lower the severity to avoid blocking migration during the > > discussion -- after all the Breaks already avoids the file conflict > > issue. > > Sorry,

Bug#1050027: Stop blocking other packages migration

2023-08-23 Thread julien . puydt
Control: severity -1 normal Hi, let's lower the severity to avoid blocking migration during the discussion -- after all the Breaks already avoids the file conflict issue. Cheers, J.Puydt

Bug#1050027: closed by Debian FTP Masters (reply to Julien Puydt ) (Bug#1050027: fixed in mathcomp-analysis 0.6.4-2)

2023-08-22 Thread julien . puydt
Le mardi 22 août 2023 à 08:34 +0200, Stéphane Glondu a écrit : > > This situation is explicitly covered in Policy 7.3 and 7.6.1. Section 7.3 explains why the Breaks is needed when there are file conflicts ; we agree on that point and hence 0.6.4-2 got it. Section 7.6 is about partial and

Bug#1010014: ITP: mathcomp-algebra-tactics -- Ring and field tactics for Mathematical Components

2022-04-22 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: mathcomp-algebra-tactics Version : 0.3.0 Upstream Author : Kazuhiko Sakaguchi * URL : https://github.com/math-comp/algebra-tactics

Bug#1010007: ITP: mathcomp-zify -- Micromega arithmetic solvers for Mathematical Components

2022-04-22 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: mathcomp-zify Version : 1.2.0+1.12+8.13 Upstream Author : Kazuhiko Sakaguchi * URL : https://github.com/math-comp/mczify * License

Re: Updating menhir

2022-04-20 Thread julien . puydt
Le vendredi 18 mars 2022 à 08:43 +0100, Ralf Treinen a écrit : > On Thu, Mar 17, 2022 at 05:20:58PM +0100, > julien.pu...@gmail.com wrote: > > > I didn't upload it because the reverse deps situation wasn't > > perfect: > > Can you upload to experimental, please ? -Ralf. > As far as I know the

Updating menhir

2022-03-17 Thread julien . puydt
Hi, I updated menhir on salsa to the last upstream -- and in the process, it got a +ds suffix because I kicked the prebuilt documentation out. I didn't upload it because the reverse deps situation wasn't perfect: - liquidsoap has an unsatisfied libogg-ocaml-dev dep) -- unrelated breakage ; -

Bug#1011347: RM: coq-float -- ROM; abandoned upstream since years

2022-05-20 Thread Julien Puydt
Package: ftp.debian.org Severity: normal X-Debbugs-Cc: jpu...@debian.org, debian-ocaml-maint@lists.debian.org This package has been abandoned upstream for years (last release tagged 2 Dec 2019). It's in FTBFS since years (bug #970453, filed Wed, 16 Sep 2020 17:19:03 +0200). I proposed its

Bug#1011648: ITP: coq-serapi -- Coq plugin for data serialization

2022-05-25 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org, jpu...@debian.org * Package name: coq-serapi Version : 0.15.0 Upstream Author : Emilio Jesús Gallego Arias et al * URL : https://github.com/ejgallego/coq-serapi

frama-c autopkgtest failing

2022-06-24 Thread julien . puydt
Hi, I thought my upload of 20220511-manganese-1.1 fixed the autopkgtest issues with the package. After all, it just worked here! But it looks like it's still failing on the Debian autopkgtest infrastructure: autopkgtest [21:19:22]: test eva: [--- [kernel] User Error: cannot

Strange problem with frama-c -- dh-ocaml's fault?

2022-06-23 Thread julien . puydt
Hi, one of frama-c's autopkgtest was failing because of: [kernel] User Error: [findlib] package 'ppx_import' not found (required by `frama-c.kernel') [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information. That was because the

Re: Comments regarding coqeal_1.1.0-1_amd64.changes

2022-07-07 Thread julien . puydt
Le mercredi 06 juillet 2022 à 21:50 +, Thorsten Alteholz a écrit : > > please also mention INRIA and University of Gothenburg in your > debian/copyright > At least they were mentioned in some file headers ... > I think I mention them in there already:

Bug#1014583: ITP: coq-equations -- Coq library to work with functions defined by equations

2022-07-08 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-equations Version : 1.3-8.15 Upstream Author : Matthieu Sozeau and Cyprien Mangin * URL : https://github.com/mattam82/Coq-Equations

Bug#1014585: ITP: coq-stdpp -- Extended standard library for Coq

2022-07-08 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-stdpp Version : 1.7.0 Upstream Author : std++ team * URL : https://gitlab.mpi-sws.org/iris/stdpp * License : BSD-3-clause

Re: coq-hott_8.15-1_amd64.changes REJECTED

2022-07-08 Thread julien . puydt
Hi, Le jeudi 07 juillet 2022 à 18:00 +, Thorsten Alteholz a écrit : > > please mention the LGPL in your debian/copyright. > Done in a new upload: coq-hott (8.15-2) unstable; urgency=medium * Drop an erroneous b-dep on ocamlgraph. * Complete d/copyright. -- Julien Puydt

Bug#1014572: ITP: coq-simple-io -- Coq plugin for purely functional IO

2022-07-08 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-simple-io Version : 1.7.0 Upstream Author : Li-yao Xia * URL : https://github.com/coq-community/coq-simple-io * License : Expat

Bug#1014048: ITP: flocq -- Floating-point arithmetic for Coq

2022-06-29 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: flocq Version : 4.1.0 Upstream Author : Sylvie Boldo, Guillaume Melquiond * URL : https://flocq.gitlabpages.inria.fr/ * License

Bug#1014610: ITP: ott -- Ott tool

2022-07-08 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: ott Version : 0.32 Upstream Author : Peter Sewell, Francesco Zappa Nardelli, Scott Owens et al * URL : https://github.com/ott-lang/ott

Re: coq-math-classes_8.15.0-1_amd64.changes REJECTED

2022-07-08 Thread julien . puydt
Hi, Le jeudi 07 juillet 2022 à 19:00 +, Thorsten Alteholz a écrit : > > please mention the LGPL and INRIA in your debian/copyright. Done: coq-math-classes (8.15.0-2) unstable; urgency=medium * Complete d/copyright. -- Julien Puydt Fri, 08 Jul 2022 08:06:04 +0200

Re: coq-equations_1.3-8.15-1_amd64.changes REJECTED

2022-07-08 Thread julien . puydt
Hi, Le vendredi 08 juillet 2022 à 23:00 +, Thorsten Alteholz a écrit : > > please also mention at least doc/* Why doc/* ? I checked again and didn't see anything special. > and INRIA, CNRS et al. in your debian/copyright. Ok, adding: Files: theories/*/Relation*.v Copyright: 1999-2018

Re: ott_0.32+ds-1_amd64.changes REJECTED

2022-07-09 Thread julien . puydt
Hi, Le samedi 09 juillet 2022 à 18:00 +, Thorsten Alteholz a écrit : > > please also mention at least the "Artistic License", the Q Public > License version 1.0 and the LGPL in your debian/copyright. I found where the Artistic and Q Public Licenses are used and completed d/copyright with

Bug#1014726: Please package new upstream

2022-07-10 Thread julien . puydt
Package: libatd-ocaml-dev Version: 2.4.1-1 Severity: wishlist I need ocaml-atd version 2.9.1 to update the elpi package. For this, I need a more recent jsonschema which we should get only in september. This report is to leave a trail of this information. Cheers, J.Puydt

Bug#1014602: ITP: coq-menhirlib -- support library for verified Menhir parsers

2022-07-08 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-menhirlib Version : 20220210 Upstream Author : Jacques-Henri Jourdan * URL : https://coquelicot.inria.fr/fpottier/menhir * License

Bug#1013949: ITP: coq-hott -- Coq library for homotopy type theory

2022-06-27 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-hott Version : 8.15 Upstream Author : Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Bas Pitters * URL : https

Bug#1013963: ITP: coq-ext-lib -- Collection of theories and plugins for Coq

2022-06-28 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-ext-lib Version : 0.11.6 Upstream Author : Gregory M. Malecha * URL : https://github.com/coq-community/coq-ext-lib * License

Bug#1013965: ITP: coqeal -- algebra and data structure algorithms for Coq

2022-06-28 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coqeal Version : 1.1.0 Upstream Author : Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles * URL : https

Bug#1014059: ITP: coq-math-classes -- Abstract interfaces for mathematical structures for Coq

2022-06-29 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-math-classes Version : 8.15.0 Upstream Author : Eelis van der Weegen, Bas Spitters, Robbert Krebbers * URL : https://github.com/coq

Bug#1014118: ITP: ocaml-pprint -- Pretty printing toolbox for OCaml

2022-06-30 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: ocaml-pprint Version : 20220103 Upstream Author : François Pottier, Nicolas Pouillard, etc * URL : https://github.com/fpottier/pprint

First draft of dh-coq

2022-06-03 Thread julien . puydt
Hi, here is some very preliminary code for dh-coq, which should avoid breaking user systems with every upload. Indeed, each time I upload one of the libcoq-* packages, it introduces inconsistent assumptions that break other packages (none or all depending on the dep graph). The goal here is that

Request: autobuild src:coq-doc

2022-06-15 Thread julien . puydt
Hi, the Coq software is DFSG-free provided by the src:coq package. But its documentation is under the OPL-1.0 -- hence not DFSG-free because of restrictions on modification [see 1 below]. In the users' interest this documentation has hence been split in a non-free src:coq-doc package providing

Bug#1014993: ITP: coq-reglang -- representation of regular languages in Coq

2022-07-15 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-reglang Version : 1.1.3 Upstream Author : Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka * URL : https://github.com/coq-community

Bug#1014997: ITP: coq-unimath -- univalent formalization of mathematics for Coq

2022-07-15 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-unimath Version : 20220204 Upstream Author : Benedikt Ahrens, Daniel Grayson, Vladimir Voevodsky * URL : https://github.com/UniMath

Bug#1014989: ITP: coq-unicoq -- enhanced unification algorithm for Coq

2022-07-15 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-unicoq Version : 1.6-8.15-1 Upstream Author : Beta Ziliani & Matthieu Sozeau * URL : https://github.com/unicoq/unicoq/ * Lic

Bug#1014991: ITP: coq-relation-algebra -- relation algebra for Coq

2022-07-15 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-relation-algebra Version : 1.7.7 Upstream Author : Damien Pous et al * URL : http://perso.ens-lyon.fr/damien.pous/ra * License

Bug#1015000: ITP: coq-quickchick -- randomized testing framework for Coq

2022-07-15 Thread Julien Puydt
Package: wnpp Severity: wishlist Owner: Julien Puydt X-Debbugs-Cc: Debian OCaml Maintainers , jpu...@debian.org * Package name: coq-quickchick Version : 1.6.3 Upstream Author : Leonidas Lampropoulos, Zoe Paraskevopoulou, Maxime Denes, Catalin Hritcu, Benjamin Pierce, Li-yao Xia

  1   2   3   4   5   >