Good news:
mizar-rs detects a pathological situation:
in the example below,
file2 (in combination with file1) is checked correctly with Mizar 8.1.12, when it shouldn't be (to be more precise, mizf accepts the file as valid but relprem helps to detect the problem).
However, mizar-rs reports a proof error for file2.
tested with commit: 19b80d99f588b1169ea774ed6ab7acccc181abab
(remember to restore the original mml.lar file after the test) :-)
cp miz/mizshare/mml.lar miz/mizshare/mml.lar.bak
head -n 326 miz/mizshare/mml.lar.bak >> miz/mizshare/mml.lar
echo "file1" >> miz/mizshare/mml.lar
echo "file2" >> miz/mizshare/mml.lar
cat >> miz/mizshare/mml/file1.miz << EOF
environ
vocabularies XBOOLE_0, FUNCT_1, STRUCT_0;
notations XBOOLE_0, STRUCT_0;
constructors STRUCT_0;
registrations STRUCT_0;
requirements BOOLE;
theorems FUNCT_2;
begin
theorem
for X,Y being non empty 1-sorted
for f being Function of X,Y holds not contradiction;
theorem
for X being 1-sorted
for Y being empty 1-sorted holds
{} is Function of X,Y by FUNCT_2:130;
EOF
cat >> miz/mizshare/mml/file2.miz << EOF
environ
vocabularies XBOOLE_0, STRUCT_0;
notations STRUCT_0;
constructors STRUCT_0;
registrations XBOOLE_0,STRUCT_0, FUNCT_2;
theorems FILE1;
begin
the non empty 1-sorted = the empty 1-sorted by FILE1:1,2;
then contradiction;
EOF
cargo run --release
[...]
RESULT:
319: calcul_1 in 2.189s
321: henmodel in 1.810s
325: struct_0 in 0.071s
326: file1 in 0.009s
[0] failed to justify 0.0 @ file2:11:45 | stirl2_1 | file2 | modal_1 | qc_trans |
327: file2 in 0.004s
283: stirl2_1 in 10.011s
313: modal_1 in 4.190s
323: qc_trans in 1.477s
324: ntalgo_1 in 1.401s
317: sublemma in 4.018s
285: nat_4 in 11.518s
290: descip_1 in 53.292s
failure: 1
success: 241787
with Mizar 8.1.12:
mizf file1.miz
Make Environment, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
-Vocabularies [ 3]
-Constructors [ 5]
-Requirements [ 7]
-Registrations [ 6]
-Notations [ 4]
-Identify [ 1]
-Reductions [ 1]
-Properties [ 1]
-Theorems [ 8]
Verifier based on More Strict Mizar Processor, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Processing: file1.miz
Parser [ 20] 0:00
MSM [ 16] 0:00
Analyzer [ 19] 0:00
Checker [ 19] 0:00
Time of mizaring: 0:00
miz2prel file1
Accommodator, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Processing: file1.miz
-Parsing
-Vocabularies [ 3]
-Constructors [ 5]
-Requirements [ 7]
-Registrations [ 6]
-Notations [ 4]
-Identify [ 1]
-Reductions [ 1]
-Properties [ 1]
-Theorems [ 8]
Exporter based on MSM Processor, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Processing: file1.miz
- Parsing [ 20]
- MSM [ 16]
- Signature [ 19]
- Theorems [ 19]
Transferer, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Theorems file is transfered into the local library
Local data base created.
mizf file2.miz
Make Environment, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
-Vocabularies [ 3]
-Constructors [ 5]
-Requirements [ 1]
-Registrations [ 6]
-Notations [ 4]
-Identify [ 6]
-Reductions [ 1]
-Properties [ 1]
-Theorems [ 7]
Verifier based on More Strict Mizar Processor, Mizar Ver. 8.1.12 (Win32/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Processing: file2.miz
Parser [ 12] 0:00
MSM [ 12] 0:00
Analyzer [ 12] 0:00
Checker [ 12] 0:00
Time of mizaring: 0:00
Good news: mizar-rs detects a pathological situation:
in the example below, file2 (in combination with file1) is checked correctly with Mizar 8.1.12, when it shouldn't be (to be more precise, mizf accepts the file as valid but relprem helps to detect the problem).
However, mizar-rs reports a proof error for file2.
tested with commit: 19b80d99f588b1169ea774ed6ab7acccc181abab (remember to restore the original mml.lar file after the test) :-)
with Mizar 8.1.12: