forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
.travis.yml
197 lines (192 loc) · 9.76 KB
/
.travis.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
# Run many verifiers on metamath files.
# We *primarily* check set.mm and iset.mm, but we also run some checks on
# other files (in particular on some HTML files).
#
# Only one verifier is necessary, but using multiple verifiers counters
# the risk that a verifier might have a defect in its implementation.
# With 4 verifiers, all 4 would have to have a defect involving an
# invalid theorem for that invalid theorem to be accepted as valid.
# This is unlikely, because the verifiers are written by different people
# in different languages. This can be considered extreme peer review, where
# every reviewer is separately checking each step.
# Some of these verifiers also check for style,
# so using multiple verifiers can also detect many different style problems.
#
# Note that one of the checks is scripts/verify.
#
# We report an error if the list of "discouraged" results is unexpected;
# this makes it easy to detect changes (which can then be specially reviewed).
# To regenerate the "discouraged" file, you can run scripts/gen-discouraged
#
# We typically rewrap the file using scripts/rewrap.
#
# Declare Linux distribution version.
# "bionic" is Ubuntu 18.04 LTS, "xenial" is Ubuntu 16, "trusty" is Ubuntu 14.
dist: bionic
# TODO: We aren't caching many old results; add caches
# (e.g., of unchanged compiled programs) to speed things further.
git:
depth: 1
sudo: false
# In each job we download, build, install, and run a verifier.
# NOTE: We generally install programs in $HOME/bin, so ensure that's on the
# PATH (usually it is on any non-Windows system).
# We use different jobs to install and run verifiers. See:
# https://docs.travis-ci.com/user/build-matrix/
jobs:
include:
###########################################################
- # smetamath-rs (smm3), a Rust verifier by Stefan O'Rear.
name: smetamath-rs (Rust, Stefan O'Rear) verification
language: rust
cache:
# Cache Rust source/executables (takes time to get and recompile)
cargo: true
timeout: 3600 # Cache for 1 hour (unit is seconds)
install:
# See https://github.com/sorear/smetamath-rs
- "[ -x ~/.cargo/bin/smetamath ] || cargo install smetamath --vers 3.0.0"
script:
- ~/.cargo/bin/smetamath --verify --split --jobs 4 --timing ./set.mm 2>&1 | tee smm.log && [ `egrep '(:Error:|:Warning:)' < smm.log; echo $?` -eq 1 ]
- ~/.cargo/bin/smetamath --verify --split --jobs 4 --timing ./iset.mm 2>&1 | tee smm.log && [ `egrep '(:Error:|:Warning:)' < smm.log; echo $?` -eq 1 ]
###########################################################
- # mmj2, a Java verifier (and more) by Mel L. O'Cat and Mario Carneiro
name: mmj2 (Java, Mel L. O'Cat and Mario Carneiro) verification
language: java
jdk:
- openjdk10
cache:
directories:
- $HOME/.m2
before_install:
- if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then export JAVA_HOME=$(/usr/libexec/java_home); fi
# Old switching system for Ubuntu 14:
# - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then jdk_switcher use "$CUSTOM_JDK"; fi
install:
# Get mmj2, a Java verifier (and more) by Mel O'Cat and Mario Carneiro
- wget -N -q http://us.metamath.org/ocat/mmj2/mmj2jar.zip
- unzip -q mmj2jar.zip
# Old switching system for Ubuntu 14:
# - jdk_switcher use oraclejdk8
script:
# Do extra checking and generate the '*discouraged.new' file
# (the 'printf' lets us insert multiple lines).
# We use setparser to check that definitions don't create syntax ambiguities
- scripts/verify-mmj2 --setparser 'mmj.verify.LRParser' --extra "$(printf 'RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel\nRunMacro,showDiscouraged,discouraged.new')" set.mm
- scripts/verify-mmj2 --setparser 'mmj.verify.LRParser' --extra "$(printf 'RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel\nRunMacro,showDiscouraged,iset-discouraged.new')" iset.mm
- echo 'Checking discouraged file:' && diff -U 0 discouraged discouraged.new
- echo 'Checking iset-discouraged file:' && diff -U 0 iset-discouraged iset-discouraged.new
###########################################################
- # Metamath.exe, the original C verifier by Norman Megill
name: Metamath.exe (ISO C, Norman Megill) verification
language: c
compiler: gcc
cache: ccache
before_install:
- gcc --version
install:
# Get metamath C program and supporting files (to validate against them)
- scripts/download-metamath
# Build/install metamath, a C verifier (and more) by Norm Megill.
- scripts/build-metamath
script:
# Create mmset.html and mmil.html so we can verify against them.
- metamath 'read set.mm' 'markup mmset.raw.html mmset.html /ALT /CSS' quit
- metamath 'read iset.mm' 'markup mmil.raw.html mmil.html /ALT /CSS' quit
- scripts/verify --top_date_skip --extra 'write bibliography mmbiblio.html' set.mm
- scripts/verify --top_date_skip iset.mm
- scripts/check-raw-html set.mm mmcomplex.raw.html mmdeduction.raw.html mmnatded.raw.html mmnf.raw.html mmset.raw.html mmzfcnd.raw.html
- scripts/check-raw-html iset.mm mmil.raw.html
# Generate HTML from raw files into mpegif-html/ and mpeuni-html/
- scripts/regen-from-raw --force '/HTML' .regened.html
- mkdir -p mpegif-html/
- for f in *.regened.html; do mv $f mpegif-html/${f%.regened.html}.html ; done
- scripts/regen-from-raw --force '/ALT_HTML' .regened.html
- mkdir -p mpeuni-html/
- for f in *.regened.html; do mv $f mpeuni-html/${f%.regened.html}.html ; done
# The following checks are arbitrarily included in the metamath job.
- echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" set.mm
- echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" iset.mm
###########################################################
- # checkmm, a C++ verifier by Eric Schmidt
name: checkmm (C++, Eric Schmidt) verification
language: cpp
compiler: gcc
cache: ccache
before_install:
- g++ --version
install:
# Get and compile checkmm, a C++ verifier by Eric Schmidt
- wget -N -q http://us.metamath.org/downloads/checkmm.cpp
- g++ -O2 -o checkmm checkmm.cpp
script:
- ./checkmm set.mm
- ./checkmm iset.mm
###########################################################
- # mmverify.py, a Python3 verifier by Raph Levien, for set.mm pre-mathbox
# This verifier takes longer than all the other verifiers (2min 14 sec).
# So we do "mathboxes" separately
# We should try to speed up the main mmverify.py culprits, e.g.,
# ./mmverify.py:299(verify), ./mmverify.py:223(apply_subst), or
# ./mmverify.py:237(decompress_proof)
name: mmverify.py (Python3, Raph Levien) set.mm verification (skipping mathboxes)
language: python
install:
- wget -N -q https://raw.githubusercontent.com/david-a-wheeler/mmverify.py/master/mmverify.py
# Python3 is very slow. We can speed it up by deleting all
# logging calls, since we don't use the logging anyway.
- sed -E '/^ *vprint\(/d' mmverify.py > mmverify.faster.py
- chmod a+x mmverify.faster.py
script:
- ./mmverify.faster.py --stop-label mathbox < set.mm
###########################################################
- # mmverify.py, a Python3 verifier by Raph Levien, for set.mm mathboxes
name: mmverify.py (Python3, Raph Levien) set.mm verification (just mathboxes)
language: python
install:
- wget -N -q https://raw.githubusercontent.com/david-a-wheeler/mmverify.py/master/mmverify.py
# Python3 is very slow. We can speed it up by deleting all
# logging calls, since we don't use the logging anyway.
- sed -E '/^ *vprint\(/d' mmverify.py > mmverify.faster.py
- chmod a+x mmverify.faster.py
script:
- ./mmverify.faster.py --begin-label mathbox < set.mm
###########################################################
- # mmverify.py, a Python3 verifier by Raph Levien, for iset.mm
name: mmverify.py (Python3, Raph Levien) iset.mm verification
language: python
install:
- wget -N -q https://raw.githubusercontent.com/david-a-wheeler/mmverify.py/master/mmverify.py
# Python3 is very slow. We can speed it up by deleting all
# logging calls, since we don't use the logging anyway.
- sed -E '/^ *vprint\(/d' mmverify.py > mmverify.faster.py
- chmod a+x mmverify.faster.py
script:
- ./mmverify.faster.py < iset.mm
###########################################################
# - # mm-scala, a Scala verifier by Mario Caneiro
# name: mm-scala (Scala)
# language: scala
# install:
# - git clone --depth 1 https://github.com/digama0/mm-scala.git
# script:
# - cd mm-scala; sbt ++$TRAVIS_SCALA_VERSION test
# - ls
# - ls mm-scala
# - mm-scala/mm-scala set.mm
###########################################################
- # Check for valid dates (detect nonsense like "June 31")
# We run scripts/report-changes.py to convert dates to Unix timestamps;
# this will raise an exception if the conversion can't occur,
# thus checking that dates are valid. If the conversion is invalid,
# you'll see the output from the last *valid* date followed by
# an exception.
# TODO: Check other .mm files, currently this only checks set.mm.
name: Date validation (of set.mm)
language: python
cache: pip
install:
- pip3 install ply
script:
- scripts/report-changes.py --gource > /dev/null
# End of jobs