Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,13 @@

(name smtml)

(version 0.14.0)

(generate_opam_files true)

(source
(github formalsec/smtml))
(source (github formalsec/smtml))

(license "MIT")

(authors
"João Pereira <[email protected]>"
Expand All @@ -26,8 +29,6 @@

(documentation "https://formalsec.github.io/smtml/smtml/index.html")

(license "MIT")

(package
(name smtml)
(synopsis "An SMT solver frontend for OCaml")
Expand All @@ -50,6 +51,7 @@
(cmdliner
(>= "1.3.0"))
dune
dune-build-info
(dolmen
(= "0.10"))
(dolmen_type
Expand Down
9 changes: 9 additions & 0 deletions scripts/create-release.sh
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,19 @@ else
TAG="$MAJOR.$MINOR.$PATCH"
fi

# Create branch
BRANCH="release/v$TAG"
git switch -c $BRANCH

# Update CHANGES.md
git-cliff -c cliff.toml -t $TAG -o CHANGES.md
git add CHANGES.md

# Update version
sed -i "s/(version .*)/(version $TAG)/" dune-project
sed -i "s/^version: \".*\"/version: \"$TAG\"/" smtml.opam
git add dune-project smtml.opam

git commit -m "Release $TAG"
git push -u origin $BRANCH

Expand Down
1 change: 1 addition & 0 deletions shell.nix
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ pkgs.mkShell {
buildInputs = with pkgs.ocamlPackages; [
bos
cmdliner
dune-build-info
dolmen_model
dolmen_type
fpath
Expand Down
2 changes: 2 additions & 0 deletions smtml.opam
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "0.14.0"
synopsis: "An SMT solver frontend for OCaml"
description:
"Smt.ml is an SMT solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability."
Expand All @@ -21,6 +22,7 @@ depends: [
"bos"
"cmdliner" {>= "1.3.0"}
"dune" {>= "3.19"}
"dune-build-info"
"dolmen" {= "0.10"}
"dolmen_type" {= "0.10"}
"dolmen_model" {= "0.10"}
Expand Down
85 changes: 55 additions & 30 deletions src/bin/cli.ml
Original file line number Diff line number Diff line change
Expand Up @@ -60,39 +60,64 @@ let from_file =
Arg.(
value & opt (some fpath) None & info [ "F"; "from-file" ] ~doc ~docv:"VAL" )

let info_run =
let doc = "Runs one or more scripts using. Also supports directory inputs" in
Cmd.info "run" ~doc
let version = Cmd_version.version

let cmd_run =
let open Term.Syntax in
let+ debug
and+ dry
and+ print_statistics
and+ no_strict_status
and+ solver_type
and+ solver_mode
and+ from_file
and+ filenames in
Cmd_run.run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
~solver_mode ~from_file ~filenames

let info_to_smt2 =
let doc = "Convert .smtml into .smt2" in
Cmd.info "to-smt2" ~doc
let info =
let doc =
"Runs one or more scripts using. Also supports directory inputs"
in
Cmd.info ~version "run" ~doc
in
let term =
let open Term.Syntax in
let+ debug
and+ dry
and+ print_statistics
and+ no_strict_status
and+ solver_type
and+ solver_mode
and+ from_file
and+ filenames in
Cmd_run.run ~debug ~dry ~print_statistics ~no_strict_status ~solver_type
~solver_mode ~from_file ~filenames
in
Cmd.v info term

let cmd_to_smt2 =
let open Term.Syntax in
let+ debug
and+ solver_type
and+ filename in
Cmd_to_smt2.run ~debug ~solver_type ~filename

let info_to_smtml =
let doc = "Print/Format the content of an .smtml file" in
Cmd.info "to-smtml" ~doc
let info =
let doc = "Convert .smtml into .smt2" in
Cmd.info ~version "to-smt2" ~doc
in
let term =
let open Term.Syntax in
let+ debug
and+ solver_type
and+ filename in
Cmd_to_smt2.run ~debug ~solver_type ~filename
in
Cmd.v info term

let cmd_to_smtml =
let open Term.Syntax in
let+ filename in
Cmd_to_smt2.run_to_smtml ~filename
let info =
let doc = "Print/Format the content of an .smtml file" in
Cmd.info ~version "to-smtml" ~doc
in
let term =
let open Term.Syntax in
let+ filename in
Cmd_to_smt2.run_to_smtml ~filename
in
Cmd.v info term

let cmd_version =
let info =
let doc = "Print smtml version and linked libraries" in
Cmd.info ~version "version" ~doc
in
let term = Term.(const Cmd_version.run $ const ()) in
Cmd.v info term

let commands =
let info = Cmd.info ~version "smtml" in
Cmd.group info [ cmd_run; cmd_to_smt2; cmd_to_smtml; cmd_version ]
15 changes: 15 additions & 0 deletions src/bin/cmd_version.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
let version_string v =
match v with None -> "n/a" | Some v -> Build_info.V1.Version.to_string v

let version = version_string @@ Build_info.V1.version ()

let run () =
Fmt.pr "version: %s@." version;
let libs = Build_info.V1.Statically_linked_libraries.to_list () in
Fmt.pr "statically linked libraries:@.";
List.iter
(fun lib ->
let name = Build_info.V1.Statically_linked_library.name lib in
let version = Build_info.V1.Statically_linked_library.version lib in
Fmt.pr "- %s (%s)@." name (version_string version) )
libs
2 changes: 1 addition & 1 deletion src/bin/dune
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@
(package smtml)
(name main)
(public_name smtml)
(libraries cmdliner smtml)
(libraries cmdliner dune-build-info smtml)
(instrumentation
(backend bisect_ppx)))
21 changes: 7 additions & 14 deletions src/bin/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,22 +15,15 @@
(* You should have received a copy of the GNU General Public License *)
(* along with this program. If not, see <https://www.gnu.org/licenses/>. *)
(***************************************************************************)
open Cmdliner

let cli =
let cmd_run = Cmd.v Cli.info_run Cli.cmd_run in
let cmd_to_smt2 = Cmd.v Cli.info_to_smt2 Cli.cmd_to_smt2 in
let cmd_to_smtml = Cmd.v Cli.info_to_smtml Cli.cmd_to_smtml in
let info = Cmd.info "smtml" in
Cmd.group info [ cmd_run; cmd_to_smt2; cmd_to_smtml ]

let returncode =
match Cmdliner.Cmd.eval_value cli with
| Ok (`Help | `Version | `Ok ()) -> Cmd.Exit.ok
| Error e -> (
match Cmdliner.Cmd.eval_value Cli.commands with
| Ok (`Help | `Version | `Ok ()) -> Cmdliner.Cmd.Exit.ok
| Error e -> begin
match e with
| `Term -> Cmd.Exit.some_error
| `Parse -> Cmd.Exit.cli_error
| `Exn -> Cmd.Exit.internal_error )
| `Term -> Cmdliner.Cmd.Exit.some_error
| `Parse -> Cmdliner.Cmd.Exit.cli_error
| `Exn -> Cmdliner.Cmd.Exit.internal_error
end

let () = exit returncode
Loading