Move jets documentation inside compiler

[gerau]

Right now we have 3 different sources in which we are getting information about Jet: LSP, codegen crate (which would generate modules for SimplicityHL-as-Rust) and simplicity-lang-org.

This PR moves Jet documentation from codegen crate to SimplicityHL compiler, which is gated behind docs feature. Also, I had added codegen executable to be distributed alongside with simplicityhl crate, also gated behind docs feature. This executable supports old behavior of generating modules, and also extends to generating JSON file with jet documentation (see BlockstreamResearch/simplicity-lang-org#42 for more context). There are launch instructions in codegen/README.md.

In future, I would like to add JetInfo as a trait for Jet, after this issue resolved, so it could also load in runtime jets documentation.

[stringhandler]

utACK 99425de

Some minor comments

[KyrylR]

Why this is deprecated?

[stringhandler]

It actually doesn't exist anymore. I'm not sure of the history of this

[schoen]

I think it does exist in low-level Simplicity but there is some reason that I don't quite understand that it's not mapped into SimplicityHL.

[KyrylR]

Verify and CheckSigVerify are uncategorized, so docs are not generated, is it Ok?

[KyrylR]

It is actually a Vector:

input_type: simplicityhl::jet::source_type(jet)
    .iter()
    .map(|ty| ty.to_string())
    .collect::<Vec<_>>()
    .join(", "),

[gerau]

Verify and CheckSigVerify are uncategorized, so docs are not generated, is it Ok?

I'm not sure what to do with them, because we cannot call this jets from SimplicityHL code (source:

SimplicityHL/src/ast.rs

Lines 1297 to 1299 in 682d829

	Ok(Elements::CheckSigVerify | Elements::Verify) | Err(_) => {
	Err(Error::JetDoesNotExist(name.clone())).with_span(from)
	}

). Verify jet is actually the same as assert! (

SimplicityHL/src/compile/mod.rs

Lines 412 to 415 in 682d829

	CallName::Assert => {
	let jet = ProgNode::jet(scope.ctx(), Elements::Verify);
	scope.with_debug_symbol(args, &jet, self)
	}

). We could mark them as "not available in SimplicityHL" instead of deprecated message as an option.

[gerau]

Verify and CheckSigVerify are uncategorized, so docs are not generated, is it Ok?

I think it is fine, because these jets are only accessible from Simplicity, and not SimplicityHL, but I would also like to hear @schoen's opinion about that as well.

[KyrylR]

Also could you align with @schoen
Here for example: https://github.com/BlockstreamResearch/simplicity-lang-org/blob/28c67437c6cef3b111339443293a672d237d72a3/jets.md.py#L45 it expects different structure of produced JSON

So if this PR is merged this should be fixed as well, as this a breaking change we should document it

[schoen]

@KyrylR I have already spoken to @gerau about the structure of the JSON and I'm not concerned about that problem (I plan to update the Python script). It is true that this is a breaking change but currently that Python script doesn't run automatically, only manually.

Related:

BlockstreamResearch/simplicity-lang-org#42

Basically, I'll have to do several things to take advantage of the work in this PR for the website, and I'm aware of the need to do them.

[schoen]

Verify and CheckSigVerify are uncategorized, so docs are not generated, is it Ok?

I think it is fine, because these jets are only accessible from Simplicity, and not SimplicityHL, but I would also like to hear @schoen's opinion about that as well.

I'd like to learn more about the history of the underlying issue, but from the point of SimplicityHL documentation, I think we should not generate docs for these jets because we can't call them from SimplicityHL, so from the point of view of SimplicityHL developers right now, it's essentially as if they don't exist in the language.

This might be a minor point suggesting that there could someday be separate documentation generated for Simplicity and for SimplicityHL, but I don't think we need to worry about that right now.