Update formatting (HarvardPL#84)

* Remove formatting in GH Action. * Apply formatting; update pom and GH action. * Add Google Java Format version. * Update Java version in CI.
aaronbembenek · Aug 27, 2024 · 55d30a7 · 55d30a7
1 parent 171c5bd
commit 55d30a7
Show file tree

Hide file tree

Showing 282 changed files with 638 additions and 943 deletions.
diff --git a/.github/workflows/maven.yml b/.github/workflows/maven.yml
@@ -15,16 +15,6 @@ on:
     branches: [ "master" ]
 
 jobs:
-  formatting:
-
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v3 # v2 minimum required
-      - uses: axel-op/googlejavaformat-action@v3
-        with:
-          args: "--replace"
-
   build:
 
     runs-on: ubuntu-latest
@@ -38,11 +28,11 @@ jobs:
     - name: Set up JDK 11
       uses: actions/setup-java@v3
       with:
-        java-version: '11'
+        java-version: '21'
         distribution: 'temurin'
         cache: maven
-    - name: Build with Maven
-      run: mvn -B package --file pom.xml
+    - name: Verify with Maven (includes building)
+      run: mvn -B verify --file pom.xml
 
     # Optional: Uploads the full dependency graph to GitHub to improve the quality of Dependabot alerts this repository can receive
     - name: Update dependency graph

diff --git a/README.md b/README.md
@@ -54,7 +54,7 @@ connecting with your SMT solver. You can compile without testing by adding the
 ### Supported SMT solvers
 
 We have primarily used Formulog with Z3 as the backend solver. Z3's textual
-interface can change even between patch versions. Z3 4.11.1 is known to work
+interface can change even between patch versions. Z3 4.12.2 is known to work
 with Formulog. To use Z3, the binary `z3` must be on your path.
 
 We also have some experimental (not recently tested) support for other solvers;
@@ -263,7 +263,8 @@ Syntax highlighting is available for Visual Studio Code (follow instructions [he
 
 Contributions to this project are most welcome!
 Please open a [GitHub issue](https://github.com/HarvardPL/formulog/issues) and then link a pull request to it.
-We use the [Google Java format](https://github.com/google/google-java-format); our CI will automatically format contributions before they are merged.
+Pull requests must be in the [Google Java format](https://github.com/google/google-java-format) before being merged.
+To reformat your code, run `mvn spotless:apply`; you can also check if your code is conformant (without reformatting it) by running `mvn spotless:check`.
 
 ## Third-party libraries
 

diff --git a/license-header b/license-header
@@ -0,0 +1,19 @@
+/*-
+ * #%L
+ * Formulog
+ * %%
+ * Copyright (C) $YEAR President and Fellows of Harvard College
+ * %%
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ * #L%
+ */
diff --git a/pom.xml b/pom.xml
@@ -1,6 +1,6 @@
 <project xmlns="http://maven.apache.org/POM/4.0.0"
-         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
-         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+    xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
     <modelVersion>4.0.0</modelVersion>
     <groupId>edu.harvard.seas.pl</groupId>
     <artifactId>formulog</artifactId>
@@ -96,16 +96,6 @@
                 <groupId>org.codehaus.mojo</groupId>
                 <artifactId>license-maven-plugin</artifactId>
                 <version>1.16</version>
-                <configuration>
-                    <inceptionYear>2018</inceptionYear>
-                    <organizationName>President and Fellows of Harvard College</organizationName>
-                    <projectName>Formulog</projectName>
-                    <licenseName>apache_v2</licenseName>
-                    <roots>
-                        <root>src/main/java</root>
-                        <root>src/test/java</root>
-                    </roots>
-                </configuration>
             </plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>
@@ -116,6 +106,29 @@
                     <target>11</target>
                 </configuration>
             </plugin>
+            <plugin>
+                <groupId>com.diffplug.spotless</groupId>
+                <artifactId>spotless-maven-plugin</artifactId>
+                <version>2.44.0.BETA2</version>
+                <configuration>
+                    <java>
+                        <googleJavaFormat>
+                            <version>1.23.0</version>
+                            <style>GOOGLE</style>
+                        </googleJavaFormat>
+                        <licenseHeader>
+                            <file>${project.basedir}/license-header</file>
+                        </licenseHeader>
+                    </java>
+                </configuration>
+                <executions>
+                    <execution>
+                        <goals>
+                            <goal>check</goal>
+                        </goals>
+                    </execution>
+                </executions>
+            </plugin>
         </plugins>
     </build>
-</project>
+</project>
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/Configuration.java b/src/main/java/edu/harvard/seas/pl/formulog/Configuration.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog;
 
 import edu.harvard.seas.pl.formulog.ast.Rule;
 import edu.harvard.seas.pl.formulog.db.IndexedFactDb;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/FormulogTester.java b/src/main/java/edu/harvard/seas/pl/formulog/FormulogTester.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2021 President and Fellows of Harvard College
+ * Copyright (C) 2021-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog;
 
 import com.fasterxml.jackson.databind.JsonNode;
 import com.fasterxml.jackson.databind.ObjectMapper;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/Main.java b/src/main/java/edu/harvard/seas/pl/formulog/Main.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog;
 
 import edu.harvard.seas.pl.formulog.ast.*;
 import edu.harvard.seas.pl.formulog.codegen.CodeGen;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/PrintPreference.java b/src/main/java/edu/harvard/seas/pl/formulog/PrintPreference.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog;
 
 public enum PrintPreference {
   EDB,

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/AbstractRule.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/AbstractRule.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 import java.util.Iterator;
 import java.util.List;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/AbstractTerm.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/AbstractTerm.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 public abstract class AbstractTerm implements Term {
 

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/BasicProgram.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/BasicProgram.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,5 +17,6 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 public interface BasicProgram extends Program<UserPredicate, BasicRule> {}
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/BasicRule.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/BasicRule.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 import java.util.Collections;
 import java.util.List;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/BindingType.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/BindingType.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 public enum BindingType {
   BOUND,

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/BoolTerm.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/BoolTerm.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 import edu.harvard.seas.pl.formulog.ast.Constructors.SolverVariable;
 import edu.harvard.seas.pl.formulog.smt.SmtLibShim;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/ComplexLiteral.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/ComplexLiteral.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 import edu.harvard.seas.pl.formulog.ast.ComplexLiterals.ComplexLiteralExnVisitor;
 import edu.harvard.seas.pl.formulog.ast.ComplexLiterals.ComplexLiteralVisitor;

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/ComplexLiterals.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/ComplexLiterals.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 public final class ComplexLiterals {
 

diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/Constructor.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/Constructor.java
@@ -1,10 +1,8 @@
-package edu.harvard.seas.pl.formulog.ast;
-
 /*-
  * #%L
  * Formulog
  * %%
- * Copyright (C) 2018 - 2020 President and Fellows of Harvard College
+ * Copyright (C) 2019-2023 President and Fellows of Harvard College
  * %%
  * Licensed under the Apache License, Version 2.0 (the "License");
  * you may not use this file except in compliance with the License.
@@ -19,6 +17,7 @@
  * limitations under the License.
  * #L%
  */
+package edu.harvard.seas.pl.formulog.ast;
 
 import edu.harvard.seas.pl.formulog.ast.Terms.TermVisitor;
 import edu.harvard.seas.pl.formulog.ast.Terms.TermVisitorExn;