Skip to content
Test PR

Allow special characters in generated Lean 4 identifiers #7175

Sign in to view logs

Allow special characters in generated Lean 4 identifiers

Allow special characters in generated Lean 4 identifiers #7175

Triggered via pull request January 8, 2025 15:02
@tothtamas28tothtamas28
opened #4729
ident-special-chars
Status Cancelled
Total duration 31s
Artifacts –

test-pr.yml

on: pull_request
Matrix: Pyk: Code Quality & Unit Tests
Java: Linting
14s
Java: Linting
Code Quality Checks
0s
Code Quality Checks
K: Ubuntu Jammy Frontend Package
0s
K: Ubuntu Jammy Frontend Package
K: Source Build & Test
0s
K: Source Build & Test
K: Ubuntu Jammy Package
0s
K: Ubuntu Jammy Package
Matrix: K: Nix Build & Test
Matrix: Pyk: Nix Build
Pyk: Documentation
0s
Pyk: Documentation
Pyk: Profiling
0s
Pyk: Profiling
Pyk: Integration Tests
0s
Pyk: Integration Tests
Pyk: Regression Tests
0s
Pyk: Regression Tests
Fit to window
Zoom out
Zoom in

Annotations

6 errors
Pyk: Code Quality & Unit Tests (3.11)
Canceling since a higher priority waiting request for 'Test PR-refs/pull/4729/merge' exists
Pyk: Code Quality & Unit Tests (3.10)
Canceling since a higher priority waiting request for 'Test PR-refs/pull/4729/merge' exists
Java: Linting
Canceling since a higher priority waiting request for 'Test PR-refs/pull/4729/merge' exists
Java: Linting
The operation was canceled.
Pyk: Code Quality & Unit Tests (3.13)
Canceling since a higher priority waiting request for 'Test PR-refs/pull/4729/merge' exists
Pyk: Code Quality & Unit Tests (3.12)
Canceling since a higher priority waiting request for 'Test PR-refs/pull/4729/merge' exists