First example-hello with dune

[elefthei]

Add --dep dune support and migrate examples/hello to dune

Summary

Adds a new --dep dune output format to fstar.exe that generates (rule ...) stanzas suitable for inclusion in dune build files. Migrates examples/hello/ (Hello and multifile)
from the old Makefile-based build to dune as a reference example.

What's new

--dep dune output format (src/parser/FStarC.Parser.Dep.fst)

• New print_dune function generates dune rules for .checked verification and OCaml/krml extraction
• Filters already-cached modules (Prims, FStar.*) from dependency lists so dune rules only reference local targets
• Handles .checked file paths in dep lists via strip_checked_suffix before module name resolution

Filepath.make_relative_to utility (src/basic/, src/ml/)

• Computes relative paths between two absolute paths, used by print_dune for output file references

examples/hello/ dune migration

• dune-project, per-subdirectory dune files with (include dune.deps.inc) and (executable ...) stanzas
• Makefile wraps dune build: generates dune.deps.inc via fstar.exe --dep dune, then calls dune build
• make clean removes generated files

Usage

Generate dune dependency rules

fstar.exe --dep dune --already_cached 'Prims FStar' Hello.fst --extract 'OCaml:Hello' > dune.deps.inc

Build from examples/hello/

cd examples/hello && make

[gebner]

Regression, revert.

[elefthei]

@copilot

[Copilot]

@elefthei I've opened a new pull request, #4102, to work on those changes. Once the pull request is ready, I'll request review from you.

[gebner]

Can we make cd examples/hello && dune build work without any setup? Calling a complicated fstar.exe command before isn't a good option.

[gebner]

Also what's up with deleting the F# test? (I realize that we don't run it during CI, but it still serves as a template to see how it should work.)

[elefthei]

Is F# supported fully, or dropped fully?

[nikswamy]

Ha, good question : ) Neither, currently.

[elefthei]

The complicated fstar.exe command produces the dependency graph as a dune file. Maybe we could add it itself to dune

[gebner]

Maybe we could add it itself to dune

That would be ideal.

[elefthei]

Cool, only dune build now no Makefile.