Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot
    Summary of the past 72 hours:
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot
    Summary of the past 72 hours:
    13351 package installations, 0 errors, 0.00% errors βœ…
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot
    Summary of the past 72 hours:
    • mathcomp-character.1.7.0:
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    15405 package installations, 3 errors, 0.02% errors

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    17459 package installations, 2 errors, 0.01% errors

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    15405 package installations, 2 errors, 0.01% errors

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    15412 package installations, 3 errors, 0.02% errors

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    17508 package installations, 0 errors, 0.00% errors βœ…

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    13394 package installations, 0 errors, 0.00% errors βœ…

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    14434 package installations, 5 errors, 0.03% errors

    Guillaume Claret
    @clarus
    menhirlib is already fixed, removing the -j option from pts...
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    17625 package installations, 1 error, 0.01% errors

    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    12541 package installations, 1 error, 0.01% errors

    Guillaume Claret
    @clarus
    problem of parallel compilation for compcert.3.1.0, cannot be fixed because sequential compilation would be too slow, added to https://github.com/coq-bench/make-html/blob/master/black_list.rb
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    9423 package installations, 1 error, 0.01% errors

    Guillaume Claret
    @clarus
    flocq-quickchick.1.0.1 is now fixed
    Karl Palmskog
    @palmskog
    I think we should open a CompCert issue about this
    they may not be aware
    Karl Palmskog
    @palmskog
    Ideally they will switch to dune at some point
    ping @ejgallego
    I think this could be a good driver for dune adoption in combined Coq/OCaml projects
    Guillaume Claret
    @clarus
    πŸ‘
    Emilio JesΓΊs Gallego Arias
    @ejgallego
    Indeed, however there is a long list of things to do w.r.t. Dune unfortunately; we just realized that due to "exports" we were not handling dependencies correctly, and a few other issues, so it will take a few more weeks to fix.
    Guillaume Claret
    @clarus
    OK
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    14674 package installations, 0 errors, 0.00% errors βœ…

    Guillaume Claret
    @clarus
    image.png
    tests for the 8.10.0 are up and running!
    Emilio JesΓΊs Gallego Arias
    @ejgallego
    :clap: :clap:
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    10560 package installations, 22 errors, 0.21% errors

    Guillaume Claret
    @clarus
    OK, the errors are due to timeouts for GeoCoq and to Coq 8.10 for the rest
    normally everything is now fixed
    Karl Palmskog
    @palmskog
    we have a multicore 8.10.0 now in OPAM thanks to Pablo, maybe restart GeoCoq?
    really nice pruning
    Guillaume Claret
    @clarus
    ah, actually Coq is compiled just once
    (for all the packages)
    and is not counted into the timeout
    thanks
    Karl Palmskog
    @palmskog
    so you cache it? Or use docker image or similar?
    Guillaume Claret
    @clarus
    I increased the timeout for dependencies to 2 hours
    I build it, cache it, then run opam install for each package
    after that I clear the cache
    (using rsync to handle the cache)
    Emilio JesΓΊs Gallego Arias
    @ejgallego
    Newer dune does also provide a binary-cache, it could imply dramatic speedups for switches
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    13795 package installations, 8 errors, 0.06% errors

    Guillaume Claret
    @clarus
    error fixed for GeoCoq, LTac2 is fixed as the missing dependency Coq 8.10 is now released
    @palmskog for coq-hammer, should there be a -j1 option for now to prevent compilation issues?
    Karl Palmskog
    @palmskog
    ah right, I will just remove the -j{jobs} for now for that old package
    Guillaume Claret
    @clarus
    OK, top!
    coq-opam-bench-gitter-bot
    @coq-opam-bench-gitter-bot

    Summary of the past 72 hours:

    14922 package installations, 1 error, 0.01% errors

    Guillaume Claret
    @clarus
    Just a temporary download error