19 Commits

Author SHA1 Message Date
Garmelon
530925c69b chore: fix test suite on macOS (#12780)
MacOS uses a very old version of bash where `"${FOO[@]}"` fails if `set
-u` is enabled and `FOO` is undefined. Newer versions of bash expand
this to zero arguments instead.

Also, `lint.py` used the shebang `#!/usr/bin/env python` instead of
`python3`, which fails on some systems.

In CI, all macos tests run on nscloud runners. Presumably, they have
installed newer versions of various software, hence this didn't break in
CI.
2026-03-03 20:59:08 +00:00
int-y1
ce4ae37c19 chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
Sebastian Ullrich
65c1bc8952 fix: gen_constants_cpp.py: mark constants as persistent 2020-11-29 18:59:39 +01:00
Leonardo de Moura
50207e2c5a chore(library/constants.txt): remove dead variables 2019-03-22 13:26:48 -07:00
Sebastian Ullrich
20451918a6 fix(library/constants): more Io -> IO 2019-03-21 15:11:05 -07:00
Sebastian Ullrich
4b3ca1f679 fix(script/gen_constants_cpp): do not insert '_' between two upper case letters 2019-03-21 15:06:45 -07:00
Leonardo de Moura
d78ad40aaf feat(script/gen_constants_cpp.py): support for provifing custom C name 2019-03-21 15:06:44 -07:00
Leonardo de Moura
9d5ab01647 fix(script/gen_constants_cpp): snake_case conversion 2019-03-21 15:06:43 -07:00
Leonardo de Moura
ef85657c90 feat(script/gen_constants_cpp): generate snake_case C++ function names 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
37e5f03351 refactor(library/system/io): move into init 2018-08-21 08:43:09 -07:00
Leonardo de Moura
3df91f1567 chore(*): fix tests 2018-05-21 06:57:43 -07:00
Leonardo de Moura
1e11611388 chore(library): cleanup constants.txt 2018-04-12 16:43:11 -07:00
Sebastian Ullrich
04f1d114a3 chore(script/gen_constants_cpp): make it run from anywhere 2017-03-09 20:30:03 -08:00
Leonardo de Moura
9d3c0497cb chore(frontends/lean): rename transient commands
See issue #1432
2017-03-09 18:41:19 -08:00
Sebastian Ullrich
4bad1bea82 chore(script/gen_*): +x 2017-03-05 08:37:16 -08:00
Sebastian Ullrich
908a7bd9f3 feat(frontends/lean/parser): expr patterns 2017-02-23 01:52:13 +01:00
Leonardo de Moura
19cf5e916b chore(script/gen_constants_cpp): generates a warning if automatically generated C++ function is not used in the source code 2017-02-21 12:05:41 -08:00
Leonardo de Moura
d1d5428808 feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes 2017-02-21 10:45:31 -08:00
Leonardo de Moura
27f6bfd3f0 refactor(*): add file constants.txt with all constants used by the Lean binary 2015-01-23 16:50:32 -08:00