Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Karl Palmskog
    @palmskog
    @yforster could you post a link to Gert Smolka's Coq-related lecture notes?
    Maxime Dénès
    @maximedenes
    @mattam82 are you around?
    Yannick Forster
    @yforster
    @palmskog Both the pdf and accompanying Coq files are linked here: https://courses.ps.uni-saarland.de/icl_19/2/Resources. Also some of the older versions are there, most notable the notes from 2014 which still contained Coq code
    Karl Palmskog
    @palmskog
    @yforster thanks, looks great! do you think there's any chance of the Coq files migrating to a public repo of some sort (e.g., Github, Gitlab) in the future?
    also, it's OK to link those from the Coq wiki right?
    Yannick Forster
    @yforster
    They are publicly accessible, so I think so. I can quickly ask Gert to make sure though
    Matthieu Sozeau
    @mattam82
    Yannick Forster
    @yforster
    @palmskog and regarding public repos... It's definitely a good idea, but it's probably only going to happen only after they have reached some sort of stabilisation
    Karl Palmskog
    @palmskog
    @yforster OK sounds good, please go ahead and ask about linking from wiki, maybe we could even list it on https://coq.inria.fr/documentation
    Jim Fehrle
    @jfehrle
    @ejgallego Ah, I didn't think to click on filenames. I hadn't heard anyone mention code coverage, so I thought was new. Is it getting much use? No coverage of printing? The number of untested paths per file would be an interesting statistic, though.
    Emilio Jesús Gallego Arias
    @ejgallego
    @jfehrle oh, I'll add printing indeed. It is fairly easy to get and process the coverage data by yourself, there are still some issues with the build system but I hope to push a full CI coverage job this summer. The tool that generates the reports has many options and I'm sure they would warmly welcome contributions, there are easier on PRs than us :) see the coverage issue in the coq repos for more details
    Jim Fehrle
    @jfehrle
    I don't quite get this. The highlighting seems to indicate 2 paths on each line where I don't see any conditionality.
    image.png
    Jim Fehrle
    @jfehrle
    @mattam82 What does "TCB" mean? Abbreviation for ??
    Karl Palmskog
    @palmskog
    Trusted Computing Base
    it's a term originally from computer security, the concept was first introduced here: http://www.csl.sri.com/users/rushby/papers/sosp81.pdf
    Théo Zimmermann
    @Zimmi48
    @CohenCyril @gares @palmskog @vbgl @maximedenes Possibly relevant discussion here: https://discuss.ocaml.org/t/package-version-source-vs-binary/3852
    Emilio Jesús Gallego Arias
    @ejgallego
    @jfehrle actually the instrumentation needs to be aware of low-level OCaml semantics, but indeed the first statement could produce an exception so there are two paths indeed.
    This could be improved with analysis of course
    Théo Zimmermann
    @Zimmi48
    ?
    Emilio Jesús Gallego Arias
    @ejgallego
    @Zimmi48 ocaml/dune#2224 maybe that's of your interest, indeed automatic version management in Dune will close over the deps
    Théo Zimmermann
    @Zimmi48
    Thanks for the link
    Emilio Jesús Gallego Arias
    @ejgallego
    Thanks to you
    Would be awesome if you had some feedback, it took Dune devs a long time to implement design this, it is tricky
    Théo Zimmermann
    @Zimmi48
    I'll try to provide some then.
    Emilio Jesús Gallego Arias
    @ejgallego
    :+1:
    Théo Zimmermann
    @Zimmi48
    It looks good to me @ejgallego. We should try to have a branch of Coq using this version of Dune to see how it would work. But I wouldn't want to duplicate work that you have already done.
    Jim Fehrle
    @jfehrle
    OK, exceptions make some sense.
    Emilio Jesús Gallego Arias
    @ejgallego
    @Zimmi48 it should work well, tho if this is going for Dune 2.0.0 then there is no urgency; I hope to advance a bit on Dune + Coq soon again.
    Matthieu Sozeau
    @mattam82
    The CUDW wiki page has been updated with information on the excursion in Antibes tomorrow, don’t forget swimming gear :)
    Emilio Jesús Gallego Arias
    @ejgallego
    and the sunscreen !
    Matthieu Sozeau
    @mattam82
    If anyone wants to join we’re having (a bit fancy) drinks at YOLO in Juan les Pins
    Maxime Dénès
    @maximedenes
    @mattam82 Thanks for taking care of the excursion!
    Jim Fehrle
    @jfehrle
    For the excursion, I guess we can leave our laptops locked in the room overnight? I don't want to be lugging a laptop around the beach.
    Karl Palmskog
    @palmskog
    SimonBoulier
    @SimonBoulier
    Here are the slides of my yesterday talk (link on the wiki also): http://perso.eleves.ens-rennes.fr/~sboul434/talks/slides_metacoq_CUDW_2019.pdf
    Karl Palmskog
    @palmskog
    :thumbsup: for slides
    MSoegtropIMC
    @MSoegtropIMC
    @tlringer : Cygwins definition of "ACRONYM": Abbreviated Coded Rendition Of Name Yielding Meaning
    Matthieu Sozeau
    @mattam82
    @herbelin @all we’re having drinks and early diner at Le bistrot de la plage in Antibes (near beach la Salis)
    Karl Palmskog
    @palmskog
    funny slides/comics on dependent types by Conor McBridge (with usual political references): http://strictlypositive.org/winging-jpgs/
    Frédéric Dabrowski
    @DabrowskiFr
    From /dev/doc/change.md
    "The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are deprecated. Use TYPED AS instead."
    According to the coqpp parser they are more than deprecated, can't find an entry for them.
    Karl Palmskog
    @palmskog
    one question that came up over lunch: best documentation resources for doing real analysis using Coq?
    Yves pointed out that Boldo & Melquiond's book covers this to some extent, but are there others?
    Matthieu Sozeau
    @mattam82
    Not that I know of. CoRN contains some, I guess Boldo's et al survey is the best reference you can find comparing different frameworks (but it's quite old already) https://hal.inria.fr/hal-00806920v1/document
    Gaëtan Gilbert
    @SkySkimmer
    evar stands for evil variable
    😎
    Karl Palmskog
    @palmskog
    for anyone who missed it, the logo/painting le coq mécanisé by Lilia Anisimova (Ilya Sergey's wife who's a professional artist/illustrator)
    Talia Ringer
    @tlringer
    ^ It's so good
    The logo