Skip to content

Commit

Permalink
Migrate from Checkstyle to Spotless (#3874)
Browse files Browse the repository at this point in the history 
This PR migrates all of our formatting checks from the Checkstyle plugin
to the Spotless plugin.

As a result, `mvn package` (or `mvn spotless:apply` or `mvn
process-sources`) automatically fixes any formatting violations, e.g.,
inserting copyright headers for you.

***The diff is large, but the only non-automated code changes are in
`pom.xml` and `src/main/config/checkstyle-*.xml`***

All the behavior is the exact same except:
- Previously, copyright headers could match the regex `Copyright \(c\)
(Runtime Verification, Inc|K Team). All Rights Reserved.`, but now we
only accept the `Runtime Verification, Inc` version due to limitations
of Spotless. All existing headers were converted automatically
- If there is an issue with this legally, I believe there is a mechanism
to avoid changing the copyright of any existing files, but all new files
would still require `Runtime Verification, Inc`
- We more broadly enforce spaces over tabs, unix line endings, newlines
at the end of each file, and no trailing whitespace. Previously, this
was only enforced for K and Java files.

---------

Co-authored-by: rv-jenkins <[email protected]>
  • Loading branch information
@Scott-Guest @rv-jenkins
Scott-Guest and rv-jenkins authored Dec 18, 2023
1 parent 1b6a9c0 commit b5c6368
Show file tree
Hide file tree
Showing 1,236 changed files with 1,475 additions and 1,493 deletions.
2 changes: 1 addition & 1 deletion CHANGELOG.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

K Framework 6.1.0
Expand Down
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

# K Framework Contributor Guide
Expand Down
2 changes: 1 addition & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
permalink: README.html
---

Expand Down
1 change: 0 additions & 1 deletion docs/ktools.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -383,4 +383,3 @@ with the kserver active it takes 2m. You can start the kserver in two ways.

Because we reuse caches, you should stop and restart the server between runs.
The Nailgun implementation hasn't been updated in the last 3-5 years, and it's not compatible with Java 18 onwards.

2 changes: 1 addition & 1 deletion k-distribution/INSTALL.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---
Installing the K Framework
==========================
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

K Builtins
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/domains.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

Basic Builtin Types in K
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/ffi.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

K Foreign Function Interface
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/json.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

Syntax of JSON
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/kast.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

K Language Features
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/prelude.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

K Prelude
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/rat.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

Rational Numbers in K
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/substitution.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

Capture-Aware Substitution in K
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/builtin/unification.k
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) K Team. All Rights Reserved.
// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
require "domains.md"
module UNIFICATION
imports SET
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/documentation.k
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) K Team. All Rights Reserved.
// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
module DOCUMENTATION
configuration <k> $PGM:K </k>
endmodule
7 changes: 3 additions & 4 deletions k-distribution/include/kframework/html/k-definition.css
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
/* Copyright (c) K Team. All Rights Reserved. */
/* Copyright (c) Runtime Verification, Inc. All Rights Reserved. */
.bold
{
font-weight: bold;
Expand Down Expand Up @@ -110,7 +110,7 @@ top : 3px;
{
color : black;
border-width: 3px;
display: inline-block;
display: inline-block;
padding: 10px;
padding-left: 20px;
padding-right: 20px;
Expand All @@ -123,7 +123,7 @@ text-align: left;
{
color : black;
border-width: 1px;
display: inline-block;
display: inline-block;
padding: 10px;
padding-left: 20px;
padding-right: 20px;
Expand Down Expand Up @@ -158,4 +158,3 @@ background-color: #f2f2f2;
border-color: #000000;
background-color: #e5e5e5;
}

6 changes: 3 additions & 3 deletions k-distribution/include/kframework/html/k-documentation.css
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
/* Copyright (c) K Team. All Rights Reserved. */
/* Copyright (c) Runtime Verification, Inc. All Rights Reserved. */
.bold
{
font-weight: bold;
Expand Down Expand Up @@ -86,7 +86,7 @@ top : 3px;
{
color : black;
border-width: 3px;
display: inline-block;
display: inline-block;
padding: 10px;
padding-left: 20px;
padding-right: 20px;
Expand All @@ -99,7 +99,7 @@ text-align: left;
{
/*color : black;
border-width: 1px;
display: inline-block;
display: inline-block;
padding: 10px;
padding-left: 20px;
padding-right: 20px;
Expand Down
71 changes: 35 additions & 36 deletions k-distribution/include/kframework/latex/k.sty
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
% Copyright (c) K Team. All Rights Reserved.
% Copyright (c) Runtime Verification, Inc. All Rights Reserved.
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{k}[2012/02/14 Package for typesetting K Framework definitions http://k-framework.org]

Expand All @@ -9,7 +9,7 @@
% \RequirePackage{etextools} % for xifstrequal
% \RequirePackage{stringstrings} % for \stringlength

\SetupKeyvalOptions{family=k,prefix=k@}
\SetupKeyvalOptions{family=k,prefix=k@}


\DeclareStringOption[bubble]{style} % the default style for cells & stuff
Expand All @@ -19,7 +19,7 @@
\ProcessKeyvalOptions*

% Usage Examples %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Next command uses the default style (bubble) with tight edges for cells.
% Next command uses the default style (bubble) with tight edges for cells.
% \usepackage[tight]{k}
%
% Next command changes the default style to mathematic cells.
Expand All @@ -41,7 +41,7 @@
% If the default was set to math, use bubble instead of math above.

% Some exported commands (useful for manually writing K):
% \kall, \kprefix, \ksuffix, and \kmiddle are used to specify cells which are
% \kall, \kprefix, \ksuffix, and \kmiddle are used to specify cells which are
% either complete, open to the right, open to the left, and open both ways,
% respectively .

Expand Down Expand Up @@ -89,7 +89,7 @@

\RequirePackage[small,compact]{titlesec}
%\titleformat{command}[shape]{format}{label}{sep}{before}[after]
% shape ::= hang | block | display | runin | leftmargin | rightmargin
% shape ::= hang | block | display | runin | leftmargin | rightmargin
% | drop | wrap | frame
% sep is mandatory to be a length.
% more on http://www.ctex.org/documents/packages/layout/titlesec.pdf
Expand Down Expand Up @@ -745,7 +745,7 @@ $\mid\;{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]\;}%
{\pgfpointanchor{current bounding box}{north east}}}
\pgfextractx{\k@cellContentWidth}{\k@cellContentBBox}%
\pgfextracty{\k@cellContentHeight}{\k@cellContentBBox}%

\begin{pgfonlayer}{background}
\ifdraft{%
\path (cell content.center)
Expand Down Expand Up @@ -826,7 +826,7 @@ rectangle,rectangle
\setlength{\k@ruptureStepSize}{\n3}%
\setlength{\k@ruptureStepSize}{.25\k@ruptureStepSize}%
}%

% Draw counter-clock-wise, starting from the
% lower right corner.
(cell body.south east)
Expand All @@ -849,7 +849,7 @@ rectangle,rectangle
% Bottom (just close the path)
-- cycle;
\end{pgfonlayer}

% Add extra space above and below the cell.
\path[use as bounding box] (current bounding box.south west) ++(0,-.3333em)
rectangle (current bounding box.north east) ++(0,.3333em);
Expand Down Expand Up @@ -918,12 +918,12 @@ rectangle,rectangle
\newcommand{\ksentence}[7][]{%
\par\indent
\k@ruleLabel{#3}{#2}\hspace{1em}$%
\ifthenelse{\equal{#1}{}}{}{%
\left(%
\ifthenelse{\equal{#1}{}}{}{%
\left(%
}%
#4%
\ifthenelse{\equal{#1}{}}{}{%
\right)%
\ifthenelse{\equal{#1}{}}{}{%
\right)%
}%
$%
\ifthenelse{\equal{#5}{}}{}{%
Expand All @@ -933,8 +933,8 @@ rectangle,rectangle
\whenEns{#6}%
}%
\k@markPosition%
\ifthenelse{\equal{#7}{}}{}{%
\ruleAttributes{#7}%
\ifthenelse{\equal{#7}{}}{}{%
\ruleAttributes{#7}%
}%
\par\ \par
}
Expand Down Expand Up @@ -974,39 +974,38 @@ rectangle,rectangle
%frame=tb,
columns=flexible,
mathescape=false,
upquote=true,
upquote=true,
% literate=
% {"}{\textquotedbl}1
}
}{}
\lstdefinelanguage{k}{
upquote=true,
upquote=true,
morekeywords={kompile, kast, krun, require, HOLE, configuration, module, end, imports, rule, macro, op, ops, syntax, sort, sorts, subsort, subsorts, context, HOLE, hybrid, strict, seqstrict, binder, color, latex, kvar, transition, superheat, supercool, search, rewrite, prec, gather, stream, multiplicity, when},
emph={[3]Map, Set, Bag, List, K, KLabel, KResult, KProper, CellLabel, SetItem, BagItem, ListItem, MapItem, Int, Bool, String, Id},
emph={[3]Map, Set, Bag, List, K, KLabel, KResult, KProper, CellLabel, SetItem, BagItem, ListItem, MapItem, Int, Bool, String, Id},
emphstyle={[3]\textit},
literate=
{LT}{$<$}3
{LEQ}{$<=$}4
% {.K}{$\kdot{\it K}$}2
% {.List}{$\kdot{\it List}$}4
{LEQ}{$<=$}4
% {.K}{$\kdot{\it K}$}2
% {.List}{$\kdot{\it List}$}4
{PROMPT}{\$}1
{...<}{${\ellipses}\langle$}2
{>}{$\rangle$}1
{>}{$\rangle$}1
{>...}{$\rangle{\ellipses}$}2
{+Int}{$+{\rm\scriptstyle Int}$}4
{*Int}{$*{\rm\scriptstyle Int}$}4
{/Int}{$/{\rm\scriptstyle Int}$}4
{LeqInt}{${<}{=}{\rm\scriptstyle Int}$}9
{!=Int}{${!}{=}{\rm\scriptstyle Int}$}5
{==Bool}{${=}{=}{\rm\scriptstyle Bool}$}7
{=/=Bool}{${=}{/}{=}{\rm\scriptstyle Bool}$}9
{notBool}{${\tt not}{\rm\scriptstyle Bool}$}5
{<}{$\langle$}1
{_}{$\_$}1 {~}{$\_$}1
{=>}{$\;=\!>$}5
{->}{{$->$}}3
{~>}{{$\sim\!\!>$}}3
{|->}{$\;|-\!\!>$}5
{+Int}{$+{\rm\scriptstyle Int}$}4
{*Int}{$*{\rm\scriptstyle Int}$}4
{/Int}{$/{\rm\scriptstyle Int}$}4
{LeqInt}{${<}{=}{\rm\scriptstyle Int}$}9
{!=Int}{${!}{=}{\rm\scriptstyle Int}$}5
{==Bool}{${=}{=}{\rm\scriptstyle Bool}$}7
{=/=Bool}{${=}{/}{=}{\rm\scriptstyle Bool}$}9
{notBool}{${\tt not}{\rm\scriptstyle Bool}$}5
{<}{$\langle$}1
{_}{$\_$}1 {~}{$\_$}1
{=>}{$\;=\!>$}5
{->}{{$->$}}3
{~>}{{$\sim\!\!>$}}3
{|->}{$\;|-\!\!>$}5
}
\newcommand{\ka}[1]{\mbox{\lstinline[language=k]{#1}}}

2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

## Part 1: Defining LAMBDA
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/NOTES.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

We now support the following line to the syntax module:
Expand Down
4 changes: 2 additions & 2 deletions k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

# Syntax Modules and Basic K Commands
Expand Down Expand Up @@ -112,4 +112,4 @@ This way, we obtain our first programming language defined using K.

Go to [Lesson 2, LAMBDA: Module Importing, Rules, Variables](../lesson_2/README.md)

[MOVIE (out of date) [4'07"]](https://youtu.be/y5Tf1EZVj8E)
[MOVIE (out of date) [4'07"]](https://youtu.be/y5Tf1EZVj8E)
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/lambda.k
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) K Team. All Rights Reserved.
// Copyright (c) Runtime Verification, Inc. All Rights Reserved.

module LAMBDA-SYNTAX
imports DOMAINS-SYNTAX
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/NOTES.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

This folder has been added after the original tutorial was made
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/lambda.k
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) K Team. All Rights Reserved.
// Copyright (c) Runtime Verification, Inc. All Rights Reserved.

require "substitution.md"

Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/NOTES.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

Substitution has been reimplemented in the meanwhile, where the fresh
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

# Module Importing, Rules, Variables
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/lambda.k
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright (c) K Team. All Rights Reserved.
// Copyright (c) Runtime Verification, Inc. All Rights Reserved.

require "substitution.md"

Expand Down
2 changes: 1 addition & 1 deletion k-distribution/pl-tutorial/1_k/1_lambda/lesson_3/NOTES.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

When we say "previous lesson" we refer to lesson 2. This will need to change
Expand Down
4 changes: 2 additions & 2 deletions k-distribution/pl-tutorial/1_k/1_lambda/lesson_3/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
---
copyright: Copyright (c) K Team. All Rights Reserved.
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

# Evaluation Strategies using Strictness
Expand Down Expand Up @@ -41,4 +41,4 @@ in order to write human readable and interesting programs.

Go to [Lesson 4, LAMBDA: Generating Documentation; Latex Attributes](../lesson_4/README.md).

[MOVIE (out of date) [2'20"]](https://youtu.be/aul1x6bd1YM)
[MOVIE (out of date) [2'20"]](https://youtu.be/aul1x6bd1YM)
Loading

0 comments on commit b5c6368

Please sign in to comment.