Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • 18:29
    herbelin synchronize #11120
  • 17:50
    ejgallego closed #11255
  • 17:50
    ejgallego closed #11254
  • 17:50

    ejgallego on master

    Fixes #11254 (not requiring coq… Merge PR #11255: Fix #11254: "c… (compare)

  • 17:06
    ejgallego synchronize #11259
  • 16:49
    ejgallego synchronize #11259
  • 16:37
    ejgallego commented #11259
  • 16:21
    herbelin synchronize #11255
  • 16:14
    herbelin synchronize #11120
  • 16:10
    herbelin synchronize #11120
  • 16:08
    fajb labeled #11263
  • 16:07
    fajb edited #11263
  • 15:56
    Zimmi48 review_request_removed #11263
  • 15:55
    Zimmi48 demilestoned #11263
  • 15:54
    Zimmi48 milestoned #11263
  • 15:54
    Zimmi48 labeled #11263
  • 15:54
    Zimmi48 labeled #11263
  • 15:54
    Zimmi48 edited #11263
  • 15:37
    fajb review_requested #11263
  • 15:37
    fajb review_requested #11263
Gaëtan Gilbert
@SkySkimmer
so like the safe env (globalize_with_summary stuff?)
Emilio Jesús Gallego Arias
@ejgallego

@ppedrot that sounds a bit strange; indeed the thing with CEPs is that they are almost always very under-specified. Designing a document manager with holes doesn't seem trivial [and I've been doing that like 2 years, mostly on dedukti]

I'd start by adding such table on the record in VernacState, there is no reason such state has to be like imperative.

Pierre-Marie Pédrot
@ppedrot
@SkySkimmer somehow
@ejgallego it need not be imperative, it just needs to be stable by module / section closing
Emilio Jesús Gallego Arias
@ejgallego

to get erased after vo creation

I wish it was as easy as that, but once you want to have incremental rebuild you need a slightly more complex design, in particular you want to store an index

Pierre-Marie Pédrot
@ppedrot
?
Emilio Jesús Gallego Arias
@ejgallego
the state in VernacState is pure so it doesn't see any of that
Pierre-Marie Pédrot
@ppedrot
it is fairly straightforward
Emilio Jesús Gallego Arias
@ejgallego
I mean you need something such as a db,
why the proofs should go away?
Pierre-Marie Pédrot
@ppedrot
I need a document global db if you wish
because by the time the vo is created the data is stored elsewhere
Emilio Jesús Gallego Arias
@ejgallego
yup you can stash it in VernacState.t
Pierre-Marie Pédrot
@ppedrot
we had a horrible hack in Declare before for that
where we would erase on the fly the body of constants stored in a vo
this got removed after the section-in-kernel PR
but now the problem with storing opaques outside of the kernel brings back more or less the same issue
Emilio Jesús Gallego Arias
@ejgallego
that will avoid complications with the STM at the cost of dumb memory management; but at least the API should be there for the upper layers to care about that
Pierre-Marie Pédrot
@ppedrot
but vernacstate is too high for my need I think?
Emilio Jesús Gallego Arias
@ejgallego

but now the problem with storing opaques outside of the kernel brings back more or less the same issue

I guess at some point you want to transfer disk writing to the document manager, in fact we are almost there but you don't need to do it right away

Pierre-Marie Pédrot
@ppedrot
mhh
Emilio Jesús Gallego Arias
@ejgallego

but vernacstate is too high for my need I think?

I think that's the right place to hook the kind of state you want

at some point there is a component that schedules what has to be checked, this is what I call the doc manager, this is the one that owns Vernacstate and the one that can be smart here.
Pierre-Marie Pédrot
@ppedrot
reading the code, the various vernacstate pieces of state do have a summary of their own
Emilio Jesús Gallego Arias
@ejgallego
what do you mean?
Pierre-Marie Pédrot
@ppedrot
there is a Summary.declare
even though they are handled specifically in vernacstate
Emilio Jesús Gallego Arias
@ejgallego
Vernacstate is the summary
Pierre-Marie Pédrot
@ppedrot
but Pcoq.state is also in the summary by itself
Emilio Jesús Gallego Arias
@ejgallego
there is not summary.declare
that's a problem with the parser I hope we can fix soon
call it "a hack"
Pierre-Marie Pédrot
@ppedrot
ok fine
Emilio Jesús Gallego Arias
@ejgallego
we try to simulate the parser being functional
it doesn't always work but also state management in the STM is not functional so the thing is a mess
Pierre-Marie Pédrot
@ppedrot
(also about to submit a PR using a type-safe API for Summary / Libobject, I am kind of getting angry at reading the very same type casts in that file btw)
Emilio Jesús Gallego Arias
@ejgallego
summary already has a type-safe API, doesn't it?
Pierre-Marie Pédrot
@ppedrot
the API is fine, I meant the implementation
we store functions that happily cast stuff around
even though we know this cannot fail
Emilio Jesús Gallego Arias
@ejgallego
I don't see what the problem is
Pierre-Marie Pédrot
@ppedrot
ugly boilerplate code
that has a runtime cost, furthermore
Emilio Jesús Gallego Arias
@ejgallego
not sure what you mean, at least for summary I measured it and the cost is small [usually] In fact there was a bug when the futures used to be able to mess with the summary where it was restored and saved thousand of times and people didn't feel it too much
if what you mean is introducing a proper interface for objects that can persist, that's a different matter
Pierre-Marie Pédrot
@ppedrot
nah
that's 1:1 extensionally
Emilio Jesús Gallego Arias
@ejgallego
and a very worthwhile goal, but still far
Pierre-Marie Pédrot
@ppedrot
stupid patch
but I'm fed with reading the same casts over and over