Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • 18:50
    JasonGross commented #10922
  • 18:37
    JasonGross commented #10921
  • 18:35
    SkySkimmer commented #10922
  • 18:30
    SkySkimmer closed #10904
  • 18:30

    SkySkimmer on master

    Define sphinx replacements for … Fix a De Bruijn bug in the comp… Merge PR #10904: Fix a De Bruij… (compare)

  • 18:29
    SkySkimmer assigned #10904
  • 18:28
    SkySkimmer commented #10911
  • 18:27
    SkySkimmer synchronize #10911
  • 18:27
    JasonGross review_requested #10911
  • 18:27
    SkySkimmer synchronize #10863
  • 18:20
    ppedrot commented #10921
  • 18:17
    ppedrot review_requested #10857
  • 18:17
    ppedrot synchronize #10857
  • 18:16
    ppedrot commented #10857
  • 18:14
    JasonGross commented #10921
  • 18:13
    JasonGross edited #10922
  • 18:09
    JasonGross labeled #10922
  • 18:09
    JasonGross labeled #10922
  • 18:09
    JasonGross opened #10922
  • 18:08
    ppedrot closed #10633
Jan-Oliver Kaiser
@Janno
The overlay thing is hard to solve, I assume
Théo Zimmermann
@Zimmi48
It is not so hard IMHO, I have proposed an idea for a while now: #6724
I still intend to proceed on this front
Jan-Oliver Kaiser
@Janno
ah, you are proposing fixing the hash. I was under the (mistaken?) impression that people didn't want that. it is definitely the sane thing to do :)
Théo Zimmermann
@Zimmi48
Fixing and updating very frequently
Jan-Oliver Kaiser
@Janno
hehehe
Karl Palmskog
@palmskog
people used to obsess about low-level tools and how to use them together, now it's an ever-changing combination of automation services and metadata
Jad Hamza
@jad-hamza
@palmskog In my case the (visible) context is very small but I'm suspecting there is something big/transparent that I'm not seeing
Karl Palmskog
@palmskog
@jad-hamza I think it's quite common for deductive tools to take a long time to fail to prove something, since they use strategies like backtracking
the cases where the proof succeeds after a long time are usually the problematic ones
Jad Hamza
@jad-hamza

I timed inversion H on this

H : Some
        (plug
           (pierce (class t)
              (core (get_option (locate (class t) fs) (fs_derive_obligation_1 A fs t pre i)))
              (layers (get_option (locate (class t) fs) (fs_derive_obligation_1 A fs t pre i)))
              (fs_derive_obligation_2 A fs t pre i)) t) = Some fs'

and it's taking 3 seconds. I made opaque these:

Opaque class. Opaque fs_derive_obligation_1. Opaque get_option. Opaque layers. Opaque core. Opaque plug. Opaque pierce. Opaque locate.
This is strange no?

Gaëtan Gilbert
@SkySkimmer
is injection any faster?
is the type implicit argument big?
Jad Hamza
@jad-hamza
No, even a bit slower! Not sure for the type arguments, I'll check but I don't think so
Maxime Dénès
@maximedenes
@ejgallego what about separating parsing and execution for error recovery
I guess you currently recover only after tactic errors
anyway, we could focus on improving the parsing state handling
Jad Hamza
@jad-hamza
I checked the types and they're all quite small
If there is nothing obvious I'll try to reduce the example
Jad Hamza
@jad-hamza
I found that the problematic functions are pierce and plug which are defined through Equations (replacing either one with dummy Admitted functions make the inversion go through easily). When printing these functions, I see this message plug is basically transparent but considered opaque for reduction. Is there a way to make these functions really opaque for all tactics?
Jad Hamza
@jad-hamza
Just found this: coq/coq#6998 Is is possible that inversion and injection and congruence are not respecting opacity?
Maxime Dénès
@maximedenes
very possible indeed
even reflexivity does not respect Opaque...
Jad Hamza
@jad-hamza
Alright. I'll wrap my functions and all of its interesting properties in a Qed ended lemma, and that should solve the issue for now
(I hope)
Maxime Dénès
@maximedenes
don't hesitate to open an issue
usually, it's not technically hard to solve this, but there are compatibility issues
however it's hard to now until we try
Jad Hamza
@jad-hamza
I gave up on reducing the example, should I post without?
Maxime Dénès
@maximedenes
maybe you can try to define an opaque c := Some x
and try inversion on c = Some y
to see if inversion just silently ignores Opaque or not
Gaëtan Gilbert
@SkySkimmer
"basically transparent" means it's some Strategy call, not Opaque
IIRC
Maxime Dénès
@maximedenes
that's the same
Jad Hamza
@jad-hamza
Posted here coq/coq#10920, thanks
I used Qed like this to hide the definition of the function, seems to work better now: https://gist.github.com/jad-hamza/579b4c357e0d2d920f556f9bcfb1a70f
Emilio Jesús Gallego Arias
@ejgallego
@maximedenes afaict we recover on all kind of errors. The reason parsing+execution is only slightly annoying is that once you manage dependencies, both are tasks so it is not such a big deal to have a parsing task that depends on the full state of some command, the scheduler will take care of it. The biggest problem I have so far is managing the dependencies! Right now the global state is a big chunk of data so rebuilds happen very often .
For UI the focus is incrementality, not parallelization which anyways in coq is gonna be quite hard to do soundly once you look at the dep graph.
Jason Gross
@JasonGross
@Zimmi48 So if I have a repo with about 25000 lines of Coq code, about 400 lines of OCaml (which is not used by the aforementioned 25000 lines of code), and another approximately 100 lines of Coq code which does depend on the OCaml code, is this classed as a library, or a plugin, or both, or neither?
Maxime Dénès
@maximedenes

afaict we recover on all kind of errors

but then you may be parsing incorrectly, right?

not parallelization which anyways in coq is gonna be quite hard to do soundly once you look at the dep graph

yeah, this I can easily imagine. The real structure of the state in Coq as it is today is very complex (lots of inter-dependencies)

Paolo G. Giarrusso
@Blaisorblade
@jad-hamza if Opaque is not enough, you can try something like stdpp's seal — example here: https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/algebra/ofe.v#L304-308
@jad-hamza by sealing, you get something that is not definitionally equal, just propositionally, plus the prop. equality
Karl Palmskog
@palmskog
@JasonGross I think Théo and I concluded before that the repo level and Coq project level may not be the same, most straightforwardly one could say your repo contains (a) a plugin with 400 LOC OCaml + 100 LOC Coq and (b) a library with 25k LOC Coq
but the most salient distinction may be that (a) is a Coq project depending on the OCaml Coq API, while (b) does not depend on the API
Jad Hamza
@jad-hamza
@Blaisorblade Ah good to know, thanks!
vlj
@vlj
What is type in type ?
Pierre-Marie Pédrot
@ppedrot
a kernel flag that turns off the constraint checking
vlj
@vlj
Ok