aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/persistent_cache.ml
AgeCommit message (Collapse)Author
2020-11-24Keep accessed objects in memory in Persistent_cache.Pierre-Marie Pédrot
2020-11-24Alternative implementation of the Micromega persistent cache.Pierre-Marie Pédrot
Instead of loading the whole file in memory, we simply load an index table associating a file position to a key hash. Cache access is then performed on the fly by unmarshalling the data whose hash corresponds and checking key equality.
2020-11-24Preserve sharing in the Micromega cache.Pierre-Marie Pédrot
For some reason it was explicitly deactivated since the file was added, but I have no idea why. Unsetting sharing would lead to potential explosive memory consumption at unmarshalling time which is not worth the minimal cost it has at marshalling time.
2020-11-17Persistent_cache.t is always OpenGaëtan Gilbert
2020-05-16[micromega] Revert bad change from 5001deed21e8f4027411cc6413a9d2b98e1bcceeEmilio Jesus Gallego Arias
Analysis by Jason Gross: > The previous semantics was to reset the file offset to 0 during the > unlock operation, unless it fails, in which case you'd roll back the > file offset to it's present position (and very dubiously not report > any issues). The new semantics say to always roll the file offset > back to it's initial position, meaning that the position is at the > end of the file after unlocking. As far as I can tell, this results > in appending marshelled blobs to the cache file on every call to > add, rather than overwriting the cache file with the marshelled blob > of the updated table. Presumably unmarshelling the concatenation of > marshelled data can result in segfaults somehow? This also explains > why the bug only shows up sometimes; you need to get the system into > a state where it writes to the cache in a way that concatenates > blobs in the right way, but once you have such a cache you'll > segfault every time you read from it. > > I think we should probably assert false in the with block, or just > remove it entirely http://man7.org/linux/man-pages/man3/lockf.3.html > doesn't say anything about lockf erroring on unlocking). If we start > seeing errors, we can turn it into a warning. Closes: #12072
2020-04-01[lib] Remove custom backtrace destroying finalizersEmilio Jesus Gallego Arias
in favor of the one in the OCaml standard library.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-04[micromega] Add numerical compatibility layer.Emilio Jesus Gallego Arias
Only significant change is in gcd / lcm which now are typed in `Z.t`
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
2019-10-03Improved handling of micromega cachesFrédéric Besson
- Specialised hash and equality functions. Avoid collisions in extreme scenarios. - Flags to disable the use of the caches. fixes #10772
2019-09-16Re-implementation of zifyFrédéric Besson
The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 2JPR
2018-10-16[micromega] remove dead codeVincent Laporte
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-05Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.Hugo Herbelin
This fixes #6286 as suggested by PMP. See details of discussion at #6286.
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Pierre Letouzey
module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-05-20Disable memoization rather than failing when files cannot be opened.Guillaume Melquiond
Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache"). Please report.
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-22Bugfix 3604 : more robust Unix.lockfFrédéric Besson
2014-03-03Fixing some generic equalities in Micromega.Pierre-Marie Pédrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Try to make the use of Unix.lockf in micromega compatible with Win32letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15684 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-21bug fix: concurrent access of persistent_cachefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14037 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-20new csdp cache + improved error messagefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-31addition of lia.cache - csdp.cache is now handled by micromega not csdpcertfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30micromega : Better parsing of formulae - smaller proof terms for Z - ↵fbesson
redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:02:45 +0000