From cfcbb94d4fd572a8783af1625bf0274194b61485 Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 13:09:04 -0800 Subject: [PATCH 1/7] fix(vector_1D_s): work around nagfor issue --- src/formal/vector_1D_s.F90 | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/formal/vector_1D_s.F90 b/src/formal/vector_1D_s.F90 index 93d1dd0..6410b31 100644 --- a/src/formal/vector_1D_s.F90 +++ b/src/formal/vector_1D_s.F90 @@ -69,7 +69,11 @@ pure module function construct_1D_vector_from_function(initializer, order, cells integer center +#ifdef NAGFOR + associate(D => self%divergence_operator_1D_) +#else associate(D => (self%divergence_operator_1D_)) +#endif associate(Dv => D .x. self%values_) divergence_1D%tensor_1D_t = tensor_1D_t(Dv(2:size(Dv)-1), self%x_min_, self%x_max_, self%cells_, self%order_) associate( & From 7f4123e9ea0b469ee3f177cfeb8168cb867fff1c Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 15:56:48 -0800 Subject: [PATCH 2/7] doc(README): add Intro and matching example output --- README.md | 62 +++++++++++++++++++++------ example/extended-gauss-divergence.F90 | 8 ++-- 2 files changed, 52 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 7db33e2..a2c1cab 100644 --- a/README.md +++ b/README.md @@ -10,9 +10,41 @@ ___________ .__ Formal: Fortran mimetic abstraction language ============================================ -_Towards a formally verifiable, tensor-calculus langauge embedded in Fortran 2028._ +_Towards an embedded domain-specific language (DSL) for tensor calculus and formal verification._ -## Examples +Introduction +------------ +Formal supports research in software abstractions for tensor calculus by providing + +- Derived types that mimic the tensor fields. +- Differential and integral operators for writing tensor calculus expressions. + +Formal's types and operators implement the discrete calculus of [Castillo & Corbino (2020)]: mimetic discretizations satisfying discrete versions of tensor calculus theorems. +Like the underlying numerical methods, Formal's software abstractiosn mimic their tensor calculus counterparts. +For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a volume $V = [0,1]^3$ bounded by a surface area $A$, the [`extended-gauss-divergence`] example program demonstrates satisfaction of the extended Gauss divergence theorem: + +$$ \iiint_V \vec{u} \cdot \nabla f dV + \iiint_V f \nabla \cdot \vec{v} dV = \iint_A f \vec{v} \cdot d\vec{A} $$ + +Running the program as follows +```fortran +fpm run --example extended-gauss-divergence --compiler flang-new --flag -O3 +``` +should produce output that includes actual program syntax: +```fortran + f = (x**2)/2 ! <-- scalar function + v = x ! <-- vector function +.SSS. (v .dot. .grad. f) * dV = .3333333330205934 +.SSS. ( f * .div. v) * dV = .16666666739857125 + -.SS. (f .x. (v .dot. dA)) = -.5000000004191649 +---------------------------------------------------- + sum = -.2220446049250313E-15 (residual) +``` +where the small residual of approximately $-.222 \times 10^{-15}$ evidences a highly accurate approximation. + +**Future work:** Formal lays a foundation for defining an DSL embedded in Fortran via template requirements, a feature of the forthcoming standard known informmally as Fortran 202Y. + +Examples +-------- See this repository's [example](./example) subdirectory for demonstrations of how to use Formal. For usage information for each example, execute something like ```bash @@ -24,8 +56,8 @@ directory as your present working directory before issuing the above `fpm run` command. Then use tab completion to enter enter the base name and delete the file extension before pressing `return`. -## Prereqisite - +Prereqisite +----------- Building and testing Formal requires the Fortran Package Manager ([`fpm`]), which can be obtained via package manager (e.g., `brew install fpm` on macOS) or by compiling the single-file concatenation of the `fpm` source that is @@ -33,20 +65,20 @@ included among the release assets. For the `fpm` 0.12.0 release, for example, compiling [fpm-0.12.0.F90] and placing the resulting executable file in your `PATH` suffices. -## Building and testing +Building and testing +-------------------- -| Vendor | Compiler | Version(s) | Build/Test Command | -|--------|-------------|------------|-------------------------------------------------------| -| GCC | `gfortran` | 14-15 | fpm test --compiler gfortran --profile release | -| GCC | `gfortran` | 13 | fpm test --compiler gfortran --profile release --flag "-ffree-line-length-none"| -| Intel | `ifx` | 2025.1.2 | FOR_COARRAY_NUM_IMAGES=1 fpm test --compiler ifx --flag "-fpp -O3 -coarray" --profile release | -| LLVM | `flang-new` | 20-21 | fpm test --compiler flang-new --flag "-O3" | -| LLVM | `flang-new` | 19 | fpm test --compiler flang-new --flag "-O3 -mmlir -allow-assumed-rank" | -| NAG | `nagfor` | 7.2 | fpm test --compiler nagfor --flag "-O3 -fpp" | + Vendor | Compiler | Version(s) Tested | Build/Test Command +--------|-------------|-------------------|------------------- + GCC | `gfortran` | 14-15 | fpm test --compiler gfortran --profile release + GCC | `gfortran` | 13 | fpm test --compiler gfortran --profile release --flag "-ffree-line-length-none" + Intel | `ifx` | 2025.1.2 | FOR_COARRAY_NUM_IMAGES=1 fpm test --compiler ifx --flag "-fpp -O3 -coarray" --profile release + LLVM | `flang-new` | 20-21 | fpm test --compiler flang-new --flag "-O3" + LLVM | `flang-new` | 19 | fpm test --compiler flang-new --flag "-O3 -mmlir -allow-assumed-rank" + NAG | `nagfor` | 7.2 Build 7242 | fpm test --compiler nagfor --flag "-O3 -fpp" **Known Issues** 1. With `fpm` versions _after_ 0.12.0, `flang-new` can be shortened to `flang`. -2. With NAG 7.2, Build 7235 or later is recommmend, but earlier builds might work. ## Documentation The [`doc/uml/class-diagram.md`] file contains a Mermaid script that generates a @@ -57,3 +89,5 @@ graphically when viewed in a web browser. [`fpm`]: https://github.com/fortran-lang/fpm [fpm-0.12.0.F90]: https://github.com/fortran-lang/fpm/releases/download/v0.12.0/fpm-0.12.0.F90 [`doc/uml/class-diagram.md`]: ./doc/uml/class-diagram.md +[Castillo & Corbino (2020)]: https://doi.org/10.1016/j.cam.2019.06.042 +[`example/extended-gauss-divergence.F90`]: ./example/extended-gauss-divergence.F90 diff --git a/example/extended-gauss-divergence.F90 b/example/extended-gauss-divergence.F90 index 9e44071..89fc8fb 100644 --- a/example/extended-gauss-divergence.F90 +++ b/example/extended-gauss-divergence.F90 @@ -88,12 +88,12 @@ program extended_gauss_divergence if (flags%grad_ .or. all_terms) then SSS_v_dot_grad_f_dV = .SSS. (v .dot. .grad. f) * dV - print '(a,g0)', ".SSS. (v .dot. .grad. f) * dV = ", SSS_v_dot_grad_f_dV + print '(a,g0)', ".SSS. (v .dot. .grad. f) * dV = ", SSS_v_dot_grad_f_dV end if if (flags%div_ .or. all_terms) then SSS_f_div_v_dV = .SSS. (f * .div. v) * dV - print '(a,g0)', ".SSS. ( f * .div. v) * dV = ", SSS_f_div_v_dV + print '(a,g0)', ".SSS. ( f * .div. v) * dV = ", SSS_f_div_v_dV end if end associate differential_volume @@ -101,8 +101,8 @@ program extended_gauss_divergence differential_area: & associate(dA => v%dA()) if (flags%vf_ .or. all_terms) then - SS_f_v_dot_dA = .SS. (f .x. (v .dot. dA)) - print '(a,g0)', " -.SS. (f .x. (v .dot. dA)) = ", -SS_f_v_dot_dA + SS_f_v_dot_dA = .SS. (f .x. (v .dot. dA)) + print '(a,g0)', " -.SS. (f .x. (v .dot. dA)) = ", -SS_f_v_dot_dA end if if (all_terms) then From dd31809086efc53aacdd4e1ddec470a0753c68a2 Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 16:13:32 -0800 Subject: [PATCH 3/7] doc(README): add funding acknowledgement --- README.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index a2c1cab..541f66b 100644 --- a/README.md +++ b/README.md @@ -15,11 +15,10 @@ _Towards an embedded domain-specific language (DSL) for tensor calculus and form Introduction ------------ Formal supports research in software abstractions for tensor calculus by providing - - Derived types that mimic the tensor fields. - Differential and integral operators for writing tensor calculus expressions. - Formal's types and operators implement the discrete calculus of [Castillo & Corbino (2020)]: mimetic discretizations satisfying discrete versions of tensor calculus theorems. + Like the underlying numerical methods, Formal's software abstractiosn mimic their tensor calculus counterparts. For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a volume $V = [0,1]^3$ bounded by a surface area $A$, the [`extended-gauss-divergence`] example program demonstrates satisfaction of the extended Gauss divergence theorem: @@ -29,7 +28,7 @@ Running the program as follows ```fortran fpm run --example extended-gauss-divergence --compiler flang-new --flag -O3 ``` -should produce output that includes actual program syntax: +produces output that includes actual program syntax: ```fortran f = (x**2)/2 ! <-- scalar function v = x ! <-- vector function @@ -67,7 +66,6 @@ compiling [fpm-0.12.0.F90] and placing the resulting executable file in your Building and testing -------------------- - Vendor | Compiler | Version(s) Tested | Build/Test Command --------|-------------|-------------------|------------------- GCC | `gfortran` | 14-15 | fpm test --compiler gfortran --profile release @@ -80,12 +78,18 @@ Building and testing **Known Issues** 1. With `fpm` versions _after_ 0.12.0, `flang-new` can be shortened to `flang`. -## Documentation +Documentation +------------- The [`doc/uml/class-diagram.md`] file contains a Mermaid script that generates a Unified Modeling Language (UML) class diagram depicting many Formal derived types and their interrelationships. GitHub's web servers render the diagram graphically when viewed in a web browser. +Funding Acknowledgment +---------------------- +Formal is a software artifact of research funded by the Competitive Portflios for Advanced Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231. + + [`fpm`]: https://github.com/fortran-lang/fpm [fpm-0.12.0.F90]: https://github.com/fortran-lang/fpm/releases/download/v0.12.0/fpm-0.12.0.F90 [`doc/uml/class-diagram.md`]: ./doc/uml/class-diagram.md From fdcef23a29db11dee0f52ade74aed9de55ad995e Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 16:29:22 -0800 Subject: [PATCH 4/7] doc(README): add "Support and Licensing" info --- README.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 541f66b..4de1f09 100644 --- a/README.md +++ b/README.md @@ -85,13 +85,21 @@ Unified Modeling Language (UML) class diagram depicting many Formal derived types and their interrelationships. GitHub's web servers render the diagram graphically when viewed in a web browser. +Support and Licensing +--------------------- +Please see [LICENSE.txt] for the copyright and license under which Formal is distributed. +To report any difficulty with building, testing, or using Formal, please submit an [issue]. +To contribute code, please submit a [pull request] from a fork of Formal. + Funding Acknowledgment ---------------------- Formal is a software artifact of research funded by the Competitive Portflios for Advanced Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231. - [`fpm`]: https://github.com/fortran-lang/fpm [fpm-0.12.0.F90]: https://github.com/fortran-lang/fpm/releases/download/v0.12.0/fpm-0.12.0.F90 [`doc/uml/class-diagram.md`]: ./doc/uml/class-diagram.md [Castillo & Corbino (2020)]: https://doi.org/10.1016/j.cam.2019.06.042 [`example/extended-gauss-divergence.F90`]: ./example/extended-gauss-divergence.F90 +[issue]: https://github.com/berkeleylab/formal/issues +[pull request]: https://github.com/berkeleylab/formal/pulls +[LICENSE.txt]: ./LICENSE.txt From a8f8ecc327c82cfb36a6d6e13169f9bf032be727 Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 17:33:21 -0800 Subject: [PATCH 5/7] doc(README): fix typos & link Correct typos and improve clarity in README. --- README.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 0270e8c..fb8c8f0 100644 --- a/README.md +++ b/README.md @@ -15,12 +15,12 @@ _Towards an embedded domain-specific language (DSL) for tensor calculus and form Introduction ------------ Formal supports research in software abstractions for tensor calculus by providing -- Derived types that mimic the tensor fields. +- Derived types that mimic the tensor fields and - Differential and integral operators for writing tensor calculus expressions. Formal's types and operators implement the discrete calculus of [Castillo & Corbino (2020)]: mimetic discretizations satisfying discrete versions of tensor calculus theorems. -Like the underlying numerical methods, Formal's software abstractiosn mimic their tensor calculus counterparts. -For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a volume $V = [0,1]^3$ bounded by a surface area $A$, the [`extended-gauss-divergence`] example program demonstrates satisfaction of the extended Gauss divergence theorem: +Like the underlying numerical methods, Formal's software abstractios mimic their tensor calculus counterparts. +For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a unit volume $V = [0,1]^3$ bounded by a surface area $A$, the program [`example/extended-gauss-divergence.F90`] demonstrates satisfaction of the extended Gauss divergence theorem: $$ \iiint_V \vec{u} \cdot \nabla f dV + \iiint_V f \nabla \cdot \vec{v} dV = \iint_A f \vec{v} \cdot d\vec{A} $$ @@ -40,7 +40,7 @@ produces output that includes actual program syntax: ``` where the small residual of approximately $-.222 \times 10^{-15}$ evidences a highly accurate approximation. -**Future work:** Formal lays a foundation for defining an DSL embedded in Fortran via template requirements, a feature of the forthcoming standard known informmally as Fortran 202Y. +**Future work:** Formal lays a foundation for defining a DSL embedded in Fortran via template requirements, a feature of the forthcoming standard known informally as Fortran 202Y. Examples -------- @@ -55,8 +55,8 @@ directory as your present working directory before issuing the above `fpm run` command. Then use tab completion to enter enter the base name and delete the file extension before pressing `return`. -Prereqisite ------------ +Prerequisite +------------ Building and testing Formal requires the Fortran Package Manager ([`fpm`]), which can be obtained via a package manager (e.g., `brew install fpm` on macOS) or by compiling the single-file concatenation of the `fpm` source that is @@ -75,7 +75,7 @@ Building and testing LLVM | `flang-new` | 19 | fpm test --compiler flang-new --flag "-O3 -mmlir -allow-assumed-rank" NAG | `nagfor` | 7.2 Build 7242 | fpm test --compiler nagfor --flag "-O3 -fpp" -With `fpm` versions _after_ 0.12.0, `flang-new` can be shortened to `flang` in the aboe `fpm` commands. +With `fpm` versions _after_ 0.12.0, `flang-new` can be shortened to `flang` in the above `fpm` commands. Documentation ------------- @@ -92,7 +92,7 @@ To contribute code, please submit a [pull request] from a fork of Formal. Funding Acknowledgment ---------------------- -Formal is a software artifact of research funded by the Competitive Portflios for Advanced Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231. +Formal is a software artifact of research funded by the Competitive Portfolios for Advanced Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231. [`fpm`]: https://github.com/fortran-lang/fpm [fpm-0.12.0.F90]: https://github.com/fortran-lang/fpm/releases/download/v0.12.0/fpm-0.12.0.F90 From 39b57d9b5a0ecd336e21494b5cb78c2d813d323a Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 17:58:39 -0800 Subject: [PATCH 6/7] doc(README) word wrap, fix typos, improve language --- README.md | 35 +++++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index fb8c8f0..6249585 100644 --- a/README.md +++ b/README.md @@ -14,13 +14,18 @@ _Towards an embedded domain-specific language (DSL) for tensor calculus and form Introduction ------------ -Formal supports research in software abstractions for tensor calculus by providing -- Derived types that mimic the tensor fields and -- Differential and integral operators for writing tensor calculus expressions. -Formal's types and operators implement the discrete calculus of [Castillo & Corbino (2020)]: mimetic discretizations satisfying discrete versions of tensor calculus theorems. +Formal supports research on mimetic software abstractions for tensor calculus by providing + +- Derived types that mimic tensor fields and +- Differential and integral operators for writing tensor expressions. + +Formal's types and operators implement the discrete calculus of [Castillo & Corbino (2020)]: +mimetic discretizations satisfying discrete versions of tensor calculus theorems. Like the underlying numerical methods, Formal's software abstractios mimic their tensor calculus counterparts. -For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a unit volume $V = [0,1]^3$ bounded by a surface area $A$, the program [`example/extended-gauss-divergence.F90`] demonstrates satisfaction of the extended Gauss divergence theorem: +For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a unit volume $V = [0,1]^3$ bounded +by a surface area $A$, the program [`example/extended-gauss-divergence.F90`] demonstrates satisfaction of the +extended Gauss divergence theorem: $$ \iiint_V \vec{u} \cdot \nabla f dV + \iiint_V f \nabla \cdot \vec{v} dV = \iint_A f \vec{v} \cdot d\vec{A} $$ @@ -40,20 +45,20 @@ produces output that includes actual program syntax: ``` where the small residual of approximately $-.222 \times 10^{-15}$ evidences a highly accurate approximation. -**Future work:** Formal lays a foundation for defining a DSL embedded in Fortran via template requirements, a feature of the forthcoming standard known informally as Fortran 202Y. +**Future work:** Formal lays a foundation for defining a DSL embedded in Fortran via template requirements, +a feature of the forthcoming standard known informally as Fortran 202Y. Examples -------- See this repository's [example](./example) subdirectory for demonstrations of how -to use Formal. For usage information for each example, execute something like: +to use Formal. For usage information for each example, execute something like ```bash fpm run --example -- --help ``` -where `base-name` is the portion of an example file name preceding the `.F90` or -`.f90` extension. To save typing in a terminal window, set the `example` -directory as your present working directory before issuing the above `fpm run` -command. Then use tab completion to enter enter the base name and delete the -file extension before pressing `return`. +replacing `` with the portion of an example file name preceding the `.F90` or +`.f90` extension. To save typing in a terminal window, set the `example` directory as +your present working directory before typing `fpm run` above. Then use tab completion to +enter a file name and delete the file extension before pressing `return` or `enter`. Prerequisite ------------ @@ -86,13 +91,15 @@ graphically when viewed in a web browser. Support and Licensing --------------------- -Please see [LICENSE.txt] for the copyright and license under which Formal is distributed. +Please see [LICENSE.txt] for the copyright and license under which Formal is distributed. To report any difficulty with building, testing, or using Formal, please submit an [issue]. To contribute code, please submit a [pull request] from a fork of Formal. Funding Acknowledgment ---------------------- -Formal is a software artifact of research funded by the Competitive Portfolios for Advanced Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231. +Formal is a software artifact of research funded by the Competitive Portfolios for Advanced +Scientific Computing Research Program of the U.S. Department of Energy, Office of Science, +Office of Advanced Scientific Computing Research under contract DE-AC02-05CH11231. [`fpm`]: https://github.com/fortran-lang/fpm [fpm-0.12.0.F90]: https://github.com/fortran-lang/fpm/releases/download/v0.12.0/fpm-0.12.0.F90 From 8deb3cfeddd339cc2ad47da9ab3a38683cada826 Mon Sep 17 00:00:00 2001 From: Damian Rouson Date: Mon, 19 Jan 2026 18:00:43 -0800 Subject: [PATCH 7/7] doc(README): fix equation Corrected the mathematical expression for the extended Gauss divergence theorem in the README. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 6249585..4b7dfb4 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ For example, given scalar and vector fields $f$ and $\vec{v}$ defined over a uni by a surface area $A$, the program [`example/extended-gauss-divergence.F90`] demonstrates satisfaction of the extended Gauss divergence theorem: -$$ \iiint_V \vec{u} \cdot \nabla f dV + \iiint_V f \nabla \cdot \vec{v} dV = \iint_A f \vec{v} \cdot d\vec{A} $$ +$$ \iiint_V (\vec{v} \cdot \nabla f) dV + \iiint_V (f \nabla \cdot \vec{v}) dV = \iint_A f \vec{v} \cdot d\vec{A} $$ Running the program as follows ```fortran