Run some pre-commit

- fix end of files
- trim trailing whitespace

Author: utensil

.devcontainer/devcontainer.bak.json

@@ -14,4 +14,4 @@
     "remoteEnv": {
         "PATH" : "${containerEnv:PATH}:/home/vscode/.elan/bin:/home/vscode/.local/bin"
     }
-}
+}

README.md

@@ -2,4 +2,4 @@
 
 A work-in-progress Lean 4 binding to [GiNaC](https://www.ginac.de/), which is an open-source symbolic computation library in C++, it has extensive algebraic capabilities, and has been specifically developed to be an engine for high energy physics applications.
 
-See [this doc](doc/ffi.md) to learn more.
+See [this doc](doc/ffi.md) to learn more.

codegen/requirements.txt

@@ -1,3 +1,3 @@
 libclang==16.0.6
 Jinja2==3.1.2
-PyYAML==6.0
+PyYAML==6.0

codegen/templates/cpp/class.cpp.j2

@@ -25,4 +25,4 @@ extern "C" LEAN_EXPORT lean_obj_res {{namespace}}_{{type.lean}}_{{method.lean}}(
 }
 {% endif %}
 {% endfor %}
-{% endblock %}
+{% endblock %}

codegen/templates/helper.j2

@@ -37,4 +37,4 @@ _ret_{{name|replace('::', '_')}}
 {% for param in params %}
 {{ sep() }}({{param.name}} : {{param.type.lean}})
 {%- endfor %}
-{%- endmacro %}
+{%- endmacro %}

codegen/templates/lean/base.lean.j2

@@ -6,4 +6,4 @@ namespace {{namespace}}
 
 {% block content %}{% endblock %}
 
-end {{namespace}}
+end {{namespace}}

codegen/templates/lean/class.lean.j2

@@ -16,4 +16,4 @@ instance : Nonempty ({{type.lean}}) := ({{type.lean}}Pointed).property
 opaque {{type.lean}}.{{method.lean}} {{list_sig_params_lean(method.params)}} : {{method.return_type.lean}}
 
 {% endfor %}
-{% endblock %}
+{% endblock %}

cpp/CppClass.h

@@ -43,4 +43,3 @@ lean_object * cppClass_make_exclusive(lean_object * o) {
     return of_cppClass(t_unique);
   }
 }
-

cpp/GinacFFI.cpp

@@ -12,7 +12,7 @@ extern "C" uint32_t my_add(uint32_t a, uint32_t b) {
 extern "C" lean_obj_res my_lean_fun() {
     symbol x("x"), y("y"), z("z");
     ex MyEx1 = sin(x + 2*y) + 3*z + 41;
-    ex MyEx2 = MyEx1 + 1;              
+    ex MyEx2 = MyEx1 + 1;
 
     cout << MyEx2 << endl;
 

cpp/Symbol.cpp

@@ -13,4 +13,3 @@ extern "C" LEAN_EXPORT lean_obj_res Ginac_Symbol_name(b_lean_obj_arg _sym) {
     auto sym = to_cppClass<symbol>(_sym);
     return lean_mk_string(sym->get_name().c_str());
 }
-

dev/prep.sh

@@ -5,4 +5,4 @@ sudo apt install -y curl wget git git-lfs clang lld libc++-dev
 sudo apt install -y libunwind-dev || true
 
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y
-source ~/.profile
+source ~/.profile

dev/run.sh

@@ -2,4 +2,4 @@
 sudo docker exec -it -u vscode -w /workspaces/ginac-lean ginac-lean bash
 
 # First time: run this in the container
-# source dev/prep.sh
+# source dev/prep.sh

doc/ffi.md

@@ -24,7 +24,7 @@ In Lean 4 unit tests, there's [a minimal FFI to C++ example](https://github.com/
 
 What EigenLean didn't explore, is to work with a non-header-only C++ library, which is the case for GiNaC, as well as many other C++ libraries. One particularly common case is that you have some C++ header and a pre-compiled shared library, whether it's due to the unavailability of the source code, or the difficulties to compile and link, including long compilation time. Its lakefiles is thus very simple and applicable only to libraries with less complications from its source code or binary distribution.
 
-This is mostly covered by [LeanInfer](https://github.com/lean-dojo/LeanInfer), which does a great job to make binary-only runtime to work with Lean, integreated with the Lake's [cloud build releases](https://github.com/leanprover/lean4/tree/master/src/lake#cloud-releases) to bundle binaries like pre-compiled linker-happy shared libraries for supported platforms. 
+This is mostly covered by [LeanInfer](https://github.com/lean-dojo/LeanInfer), which does a great job to make binary-only runtime to work with Lean, integreated with the Lake's [cloud build releases](https://github.com/leanprover/lean4/tree/master/src/lake#cloud-releases) to bundle binaries like pre-compiled linker-happy shared libraries for supported platforms.
 
 Some limitations of LeanInfer's solution: At the time of writing, it relies on local builds by the authors, including building LLVM, Clang and its standard library `libc++` from source, no CI has been set up to run this continuously to make it applicable for other projects. It also requires to build the C++ part with `clang++` and its standard library `libc++` on all platforms, which could be chanllenaging for FFI binding developers who are not familiar with C++ toolchains, also some libraries requires heavy patching to compile and link with `libc++` instead of the more widely available `libstdc++` from GNU.
 
@@ -89,5 +89,3 @@ Some possible future explorations:
 - the binding generating capability can become a spin-off project, which can be reused in other Lean 4 binding projects
 - explore creating bindings to Rust libraries(e.g. [egglog](https://github.com/egraphs-good/egglog/)) and making them idiomatic in Lean, like [egglog's Python binding](https://egg-smol-python.readthedocs.io/en/latest/)
 - explore reverse-FFI, i.e. calling Lean functions from C++/Rust code, even from JavaScript in the browser provided [Lean 4 WASM build makes progress](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/wasm.20build)
-
-

lakefile.lean

@@ -7,7 +7,7 @@ package «GinacLean» where
   -- preferReleaseBuild := get_config? noCloudRelease |>.isNone
   buildType := BuildType.debug
   -- buildArchive? := is_arm? |>.map (if · then "arm64" else "x86_64")
-  moreLinkArgs := #[s!"-L{__dir__}/build/lib", 
+  moreLinkArgs := #[s!"-L{__dir__}/build/lib",
     -- "-L/usr/bin/../lib/gcc/aarch64-linux-gnu/11 -L/lib/aarch64-linux-gnu -L/usr/lib/aarch64-linux-gnu -L/usr/lib/llvm-14/bin/../lib -L/lib -L/usr/lib",
     "-lginac_ffi", "-lginac", "-lcln", "-lstdc++"] -- "-v",  --, "-lc++", "-lc++abi", "-lunwind"] -- "-lstdc++"]
   weakLeanArgs := #[
@@ -18,7 +18,7 @@ package «GinacLean» where
 lean_lib «GinacLean» where
   roots := #[`Ginac]
   moreLinkArgs := #[s!"-L{__dir__}/build/lib",
-  "-lginac_ffi", 
+  "-lginac_ffi",
   "-lstdc++"]
   extraDepTargets := #["libginac_ffi"]
 
@@ -173,7 +173,7 @@ target libginac_ffi pkg : FilePath := do
   ]
 
   let mut buildJobs : Array (BuildJob FilePath) := Array.mkEmpty srcFiles.size
-    
+
   for srcFile in srcFiles do
     let job ← buildCpp pkg srcFile [ginac, cln]
     buildJobs := buildJobs.push job
@@ -214,4 +214,4 @@ script clear := do
   removeDirIfExists s!"{__dir__}/build/ir/"
   removeDirIfExists s!"{__dir__}/build/lib/examples"
   removeDirIfExists s!"{__dir__}/build/lib/Ginac"
-  return 0
+  return 0

lean/Ginac/Symbol.lean

@@ -10,4 +10,4 @@ opaque Symbol.mk (name : @&String) : Symbol
 @[extern "Ginac_Symbol_name"]
 opaque Symbol.name : Symbol → String
 
-end Ginac
+end Ginac