diff options
| author | Gaëtan Gilbert | 2019-11-08 21:40:57 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-13 15:27:13 +0100 |
| commit | a0c02da54bfedeaaa73b1188c3e2e0cd9a4e086b (patch) | |
| tree | e28165b0a567c78296f2c075ccadf25ce27ef0bb /doc | |
| parent | 7cde333abd7a1c25765a9438d1b830a133a15498 (diff) | |
Native compute: cleanup temporary files on program exit
We make a temporary directory for these files and cleanup at process
exit. The temporary directory means we don't have to guess what
extensions ocaml will produce, we can just delete everything there.
We use Lazy to avoid spamming unused directories when ahead-of-time
compiling without actually using native casts / nativenorm (typically
stdlib files).
Sadly ocaml has "create temp file" but not "create temp dir", so we
have to copy the name generation code.
Fix #10495
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/01-kernel/11081-native-cleanup.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst new file mode 100644 index 0000000000..b3e3a78b96 --- /dev/null +++ b/doc/changelog/01-kernel/11081-native-cleanup.rst @@ -0,0 +1,4 @@ +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory. (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). |