Frédéric Blanqui
Frédéric Blanqui
Indeed, I had a ~/.config/dune/github.token file which expired. It would be nice to add this in your README.md file that, in case of problems, one can try to remove ~/.config/dune/github.token....
To avoid discrepancies between the two, I suggest to have README refer to the opam file.
What's the point of keeping a proof of a 'theorem' in memory once it is checked? The dko could simply store the type but not the proof. Le 24/06/2019 à...
What do you mean by "shared"? The 'theorem' keyword has been introduced in Dedukti to denote an opaque definition: its actual content is irrelevant and can be erased; only the...
I'm afraid that, currently, LP stores proofs... @rlepigre ?
@francoisthire, there's something I don't understand. If, indeed, in Dedukti, proofs are not recorded in dko files, why are dko files as big as dk files? @EmilieGrienenberger, could you please...
Hello Emilie. Could you please give us more context and data: - Where are the files coming from? - What is the size in Mo (du -h) of a tar.gz...
In particular, how many thm do you have in average in each file?
I moved it to http://deducteam.gforge.inria.fr/lib/hollight2dk.tar.gz so that it is accessible to non Deducteam members (and also because we usually do not put big generated files under git).