We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
One test in the suite fails for me:
1366/1441 Testing: leanittest_complete_trailing_period.lean 1366/1441 Test: leanittest_complete_trailing_period.lean Command: "/opt/local/bin/bash" "./test_single.sh" "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_lean/lean/work/build/shell/lean" "complete_trailing_period.lean" Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_lean/lean/work/lean-3.51.1/src/../tests/lean/interactive "leanittest_complete_trailing_period.lean" start time: Sep 03 17:55 CST Output: ---------------------------------------------------------- --- complete_trailing_period.lean.expected.out 2023-05-25 01:58:24.000000000 +0800 +++ complete_trailing_period.lean.produced.out 2024-09-03 17:55:06.000000000 +0800 @@ -1,2 +1,2 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"kind":"definition","source":,"text":"foo.rec","type":"Π (motive : foo → Sort l) (n : foo), motive n"},{"kind":"definition","source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (motive : foo → Sort l) (n : foo), motive n"},{"kind":"inductive","source":{"column":10,"line":3},"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6} +{"completions":[],"prefix":"foo.","response":"ok","seq_num":6} ERROR: file complete_trailing_period.lean.produced.out does not match complete_trailing_period.lean.expected.out <end of output> Test time = 0.37 sec ---------------------------------------------------------- Test Failed. "leanittest_complete_trailing_period.lean" end time: Sep 03 17:55 CST "leanittest_complete_trailing_period.lean" time elapsed: 00:00:00
System info:
36-25% lean --version Lean (version 3.51.1, Release) 36-25% sw_vers ProductName: Mac OS X ProductVersion: 10.6 BuildVersion: 10A190 36-25% uname -p powerpc 36-25% /opt/local/bin/gcc-mp-14 -v Using built-in specs. COLLECT_GCC=/opt/local/bin/gcc-mp-14 COLLECT_LTO_WRAPPER=/opt/local/libexec/gcc/powerpc-apple-darwin10/14.2.0/lto-wrapper Target: powerpc-apple-darwin10 Configured with: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_lang_gcc14/gcc14/work/gcc-14.2.0/configure --prefix=/opt/local --build=powerpc-apple-darwin10 --enable-languages=c,c++,objc,obj-c++,lto,fortran,jit --libdir=/opt/local/lib/gcc14 --infodir=/opt/local/share/info --mandir=/opt/local/share/man --datarootdir=/opt/local/share/gcc-14 --with-local-prefix=/opt/local --with-system-zlib --disable-nls --program-suffix=-mp-14 --with-gxx-include-dir=/opt/local/include/gcc14/c++/ --with-gmp=/opt/local --with-mpfr=/opt/local --with-mpc=/opt/local --with-isl=/opt/local --with-zstd=/opt/local --enable-checking=release --disable-multilib --enable-lto --enable-libstdcxx-time --without-build-config --with-as=/opt/local/bin/as --with-ld=/opt/local/bin/ld --with-ar=/opt/local/bin/ar --with-bugurl=https://trac.macports.org/newticket --enable-host-shared --with-darwin-extra-rpath=/opt/local/lib/libgcc --with-libiconv-prefix=/opt/local --disable-tls --with-gxx-libcxx-include-dir=/opt/local/libexec/gcc14/libc++/include/c++/v1 --with-pkgversion='MacPorts gcc14 14.2.0_1+stdlib_flag' Thread model: posix Supported LTO compression algorithms: zlib zstd gcc version 14.2.0 (MacPorts gcc14 14.2.0_1+stdlib_flag)
The text was updated successfully, but these errors were encountered:
No branches or pull requests
One test in the suite fails for me:
System info:
The text was updated successfully, but these errors were encountered: