Small edit

README.md

@@ -44,81 +44,50 @@ Leanstral offers these capabilities:
 
 ### Mistral-Vibe
 
-Use `Leanstral 119B A6B` with [Mistral Vibe](https://github.com/mistralai/mistral-vibe). Install the latest version (2.5.0):
+Use `Leanstral 119B A6B` with [Mistral Vibe](https://github.com/mistralai/mistral-vibe). Install the latest version:
 
 ```sh
 uv pip install mistral-vibe --upgrade
-
-# make sure it's >= 2.5.0
-```
-
-Leanstral can be added by starting `vibe` and simply running:
-
-```
-/leanstall
 ```
 
-This will add `leanstral` as an additional model, add a system prompt (see [LEAD.md](https://huggingface.co/mistralai/Leanstral-2603/blob/main/LEAN.md)) as well as 
-ensure `leanstral` can be used as a subagent.
-
-
-![Screenshot 2026-03-16 at 18.03.39](https://cdn-uploads.huggingface.co/production/uploads/5dfcb1aada6d0311fd3d5448/Sm_mBI7u4XTjlKGzdXQqe.png)
-
-Then just press "tab+shift" a couple times until you see the new "lean" mode and `leanstral` model.
-
-![Screenshot 2026-03-16 at 18.17.04](https://cdn-uploads.huggingface.co/production/uploads/5dfcb1aada6d0311fd3d5448/DHwtKamfj2QfMv0TkJK6G.png)
-
-**Local server**
-
-If instead of pinging the Mistral API, you want to use your local vLLM server, you can do the following:
-- 1. Spin up a vllm server as explained in [`Usage - vllm`](#vllm-recommended)
-- 2. Create a new agent file called `lean.toml` in `~/.vibe/agents`:
+**Add as a provider** In vibe, use the `/leanstall` command.
 
-```sh
-mkdir ~/.vibe/agents/ && touch ~/.vibe/agents/lean.toml
-```
-
-And then copy-paste the following config into `~/.vibe/agents/lean.toml`
+**Local server (via vLLM):**
 
 ```toml
-display_name = "Lean (local vLLM)"
-description = "Lean 4 mode using local vLLM"
-safety = "neutral"
-
-system_prompt_id = "lean"
-active_model = "leanstral"
-
 [[providers]]
 name = "vllm"
 api_base = "http://<your-host-url>:8000/v1"
-api_key_env_var = ""
-backend = "generic"
+reasoning_as_structured_content = true
 reasoning_field_name = "reasoning_content"
-
 [[models]]
-name = "mistralai/Leanstral-2603"
-provider = "vllm"
+name = "labs-leanstral-2603"
+provider = "mistral-testing"
 alias = "leanstral"
 thinking = "high"
 temperature = 1.0
-auto_compact_threshold = 168000
-
-[tools.bash]
-default_timeout = 1200
 ```
 
-**Note**: Make sure to overwrite `<your-host-url>` with your server's url.
+**System prompt & agent**:
 
-Then restart `vibe` and "tab-shift" to "lean" mode.
+Add `~/.vibe/prompts/lean.toml` as in [LEAN.md](https://huggingface.co/mistralai/Leanstral-2603/blob/main/LEAN.md) and create `~/.vibe/agents/lean.toml`:
+
+```toml
+name = "lean"
+display_name = "Lean"
+description = "Specialized mode for Lean 4 code analysis, proof assistance, and theorem proving"
+safety = "neutral"
+agent_type = "agent"
+system_prompt_id = "lean"
+```
 
-Give it a try on some "lean" code such as, *e.g.*: [PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)
+Example repository: [PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)
 
 ### Local Deployment
 
 The model can also be deployed with the following libraries, we advise everyone to use the Mistral AI API if the model is subpar with local serving:
 - [`vllm (recommended)`](https://github.com/vllm-project/vllm): See [here](#vllm-recommended).
 - [`transformers`](https://github.com/huggingface/transformers): WIP ⏳ - follow updates on [this PR](https://github.com/huggingface/transformers/pull/44760).
-- [`SGLang`](https://github.com/sgl-project/sglang): WIP ⏳ - follow updates on [this PR](https://github.com/sgl-project/sglang/pull/20708/)
 
 #### vLLM (recommended)
 
@@ -126,32 +95,52 @@ We recommend using this model with the [vLLM library](https://github.com/vllm-pr
 
 **_Installation_**
 
-1. Make sure to install **vllm nightly**:
+> [!Tip]
+> We recommend installing vLLM from our custom Docker image that has fixes for
+> Tool Calling and Reasoning parsing in vLLM and uses the latest version of Transformers.
+> We're working with the vLLM team to merge these fixes to main as soon as possible.
+
+**_Custom Docker_**
+
+Make sure to use the following docker image [mistralllm/vllm-ms4:latest](https://hub.docker.com/repository/docker/mistralllm/vllm-ms4/latest/):
+
+```
+docker pull mistralllm/vllm-ms4:latest
+docker run -it mistralllm/vllm-ms4:latest
+```
+
+**_Manual Install_**
+
+If you prefer, you can also manually install `vllm` from this PR: [Add Mistral Guidance](https://github.com/vllm-project/vllm/pull/37081).
+
+**Note**: 
+It is likely that this PR will be split into smaller PRs and merged to `vllm` main in the coming 1-2 weeks (Stand: 16.03.2026).
+Check latest developments directly on the [PR](https://github.com/vllm-project/vllm/pull/37081).
 
-   ```
-   uv pip install -U vllm \
-       --torch-backend=auto \
-       --extra-index-url https://wheels.vllm.ai/nightly
-   ```
+1. Git clone vLLM:
+```
+git clone --branch fix_mistral_parsing https://github.com/juliendenize/vllm.git
+```
 
-   Doing so should automatically install [`mistral_common >= 1.11.0`](https://github.com/mistralai/mistral-common/releases/tag/v1.11.0).
-  
-   To check:
-   ```
-   python -c "import mistral_common; print(mistral_common.__version__)"
-   ```
-  
-   You can also make use of a ready-to-go [docker image](https://github.com/vllm-project/vllm/blob/main/docker/Dockerfile) or on the [docker hub](https://hub.docker.com/layers/vllm/vllm-openai/nightly).
+2. Install with pre-compiled kernels
+```
+VLLM_USE_PRECOMPILED=1 pip install --editable .
+```
 
-2. Install `transformers` from main:
+3. Make sure, `transformers` is installed from "main":
+```
+pip install git+https://github.com/huggingface/transformers.git
+```
 
-   ```bash
-   uv pip install git+https://github.com/huggingface/transformers.git
-   ```
+Also make sure to have installed [`mistral_common >= 1.10.0`](https://github.com/mistralai/mistral-common/releases/tag/v1.10.0).
+To check:
+```
+python -c "import mistral_common; print(mistral_common.__version__)"
+```
 
 **_Launch server_**
 
-We recommend that you use Leanstral in a server/client setting. 
+We recommand that you use Leanstral in a server/client setting. 
 
 ```
 vllm serve mistralai/Leanstral-2603 \
@@ -328,9 +317,3 @@ _Example Tool Calls_:
 `Function(arguments='{"code": "inductive State where\\n  | idle\\n  | busy\\n  | error\\n\\ndef transition : State → State → Bool\\n  | .idle, .busy => true\\n  | .busy, .idle => true\\n  | .busy, .error => true\\n  | _, _ => false\\n\\n#eval transition .idle .busy"}', name='lean_run_code')`
 
 </details>
-
-## License
-
-This model is licensed under the [Apache 2.0 License](https://www.apache.org/licenses/LICENSE-2.0.txt).
-
-*You must not use this model in a manner that infringes, misappropriates, or otherwise violates any third party’s rights, including intellectual property rights.*

chat_template.jinja

@@ -1,234 +0,0 @@
-{#- Default system message if no system prompt is passed. #}
-{%- set default_system_message = '' %}
-
-{#- Begin of sequence token. #}
-{{- bos_token }}
-
-
-{#- Handle system prompt if it exists. #}
-{%- set loop_messages = messages %}
-{%- if messages[0]['role'] != 'system' and default_system_message != '' %}
-    {{- '[SYSTEM_PROMPT]' + default_system_message + '[/SYSTEM_PROMPT]' }}
-{%- endif %}
-
-
-{#- Tools and model settings definition #}
-{%- set available_tools = '' %}
-{%- set has_tools = false %}
-{%- if tools is defined and tools is not none and tools|length > 0 %}
-    {%- set has_tools = true %}
-    {%- set available_tools = '[AVAILABLE_TOOLS]' + (tools| tojson) + '[/AVAILABLE_TOOLS]' %}
-{%- endif %}
-{%- if reasoning_effort is not defined or reasoning_effort is none %}
-    {%- set reasoning_effort = 'none' %}
-{%- endif %}
-{%- if reasoning_effort not in ['none', 'high'] %}
-    {{- raise_exception('reasoning_effort must be either "none" or "high"') }}
-{%- endif %}
-{%- set model_settings = '[MODEL_SETTINGS]{"reasoning_effort": "' + reasoning_effort + '"}[/MODEL_SETTINGS]' %}
-
-{#- Macros #}
-{%- macro render_content(content, context_name, supported_types_desc, support_thinking, support_images) -%}
-    {%- if content is string -%}
-        {{- content -}}
-    {%- elif content -%}
-        {%- for block in content -%}
-            {%- if block['type'] == 'text' -%}
-                {{- block['text'] -}}
-            {%- elif support_thinking and block['type'] == 'thinking' -%}
-                {{- '[THINK]' + block['thinking'] -}}
-                {%- if block.get('closed', true) -%}{{- '[/THINK]' -}}{%- endif -%}
-            {%- elif support_images and block['type'] in ['image', 'image_url'] -%}
-                {{- '[IMG]' -}}
-            {%- else -%}
-                {{- raise_exception('Only ' + supported_types_desc + ' chunks are supported in ' + context_name + '.') -}}
-            {%- endif -%}
-        {%- endfor -%}
-    {%- else -%}
-        {{- raise_exception(context_name + ' must have non-empty content.') -}}
-    {%- endif -%}
-{%- endmacro -%}
-
-{#- Aggregate consecutive messages with the same role except system and tool. #}
-{#- A sentinel message is appended so the last group gets flushed inside the loop. #}
-{%- set ns_agg = namespace(messages=[], current_group=[], current_role=none) %}
-{%- for message in loop_messages + [{'role': '__sentinel__'}] %}
-    {%- if message['role'] != ns_agg.current_role or message['role'] == 'system' or message['role'] == 'tool' %}
-        {%- if ns_agg.current_role == 'tool' %}
-            {%- set ns_agg.messages = ns_agg.messages + ns_agg.current_group %}
-        {%- elif ns_agg.current_role is not none %}
-            {%- set ns_c = namespace(text_parts=[], chunks=[], has_non_text=false, tool_calls=[]) %}
-            {%- for msg in ns_agg.current_group %}
-                {#- Convert reasoning / reasoning_content to a leading thinking chunk. #}
-                {%- set reasoning = msg.get('reasoning_content', msg.get('reasoning', none)) %}
-                {%- if reasoning is not none and reasoning != '' %}
-                    {%- if msg['content'] is not none and msg['content'] is not string %}
-                        {%- for block in msg['content'] %}
-                            {%- if block['type'] == 'thinking' %}
-                                {{- raise_exception('Message cannot have both thinking chunks in content and a top-level `reasoning` or `reasoning_content` field.') }}
-                            {%- endif %}
-                        {%- endfor %}
-                    {%- endif %}
-                    {%- set think_chunk = {'type': 'thinking', 'thinking': reasoning} %}
-                    {%- if msg['content'] is string and msg['content'] != '' %}
-                        {%- set new_content = [think_chunk, {'type': 'text', 'text': msg['content']}] %}
-                    {%- elif msg['content'] is not none and msg['content'] is not string and msg['content'] | length > 0 %}
-                        {%- set new_content = [think_chunk] + msg['content'] | list %}
-                    {%- else %}
-                        {%- set new_content = [think_chunk] %}
-                    {%- endif %}
-                    {%- if msg['tool_calls'] is defined and msg['tool_calls'] is not none %}
-                        {%- set msg = {'role': msg['role'], 'content': new_content, 'tool_calls': msg['tool_calls']} %}
-                    {%- else %}
-                        {%- set msg = {'role': msg['role'], 'content': new_content} %}
-                    {%- endif %}
-                {%- endif %}
-                {%- if msg['content'] is string %}
-                    {%- set ns_c.text_parts = ns_c.text_parts + [msg['content']] %}
-                {%- elif msg['content'] is not none %}
-                    {%- set ns_msg = namespace(msg_text_parts=[]) %}
-                    {%- for block in msg['content'] %}
-                        {%- if block['type'] == 'text' %}
-                            {%- set ns_msg.msg_text_parts = ns_msg.msg_text_parts + [block['text']] %}
-                        {%- else %}
-                            {%- if ns_msg.msg_text_parts | length > 0 %}
-                                {%- set ns_c.text_parts = ns_c.text_parts + [ns_msg.msg_text_parts | join('')] %}
-                                {%- set ns_msg.msg_text_parts = [] %}
-                            {%- endif %}
-                            {%- if ns_c.text_parts | length > 0 %}
-                                {%- set ns_c.chunks = ns_c.chunks + [{'type': 'text', 'text': ns_c.text_parts | join('\n\n')}] %}
-                                {%- set ns_c.text_parts = [] %}
-                            {%- endif %}
-                            {%- set ns_c.chunks = ns_c.chunks + [block] %}
-                            {%- set ns_c.has_non_text = true %}
-                        {%- endif %}
-                    {%- endfor %}
-                    {%- if ns_msg.msg_text_parts | length > 0 %}
-                        {%- set ns_c.text_parts = ns_c.text_parts + [ns_msg.msg_text_parts | join('')] %}
-                    {%- endif %}
-                {%- endif %}
-                {%- if msg['tool_calls'] is defined and msg['tool_calls'] is not none %}
-                    {%- set ns_c.tool_calls = ns_c.tool_calls + msg['tool_calls'] | list %}
-                {%- endif %}
-            {%- endfor %}
-            {%- if ns_c.has_non_text %}
-                {%- if ns_c.text_parts | length > 0 %}
-                    {%- set ns_c.chunks = ns_c.chunks + [{'type': 'text', 'text': ns_c.text_parts | join('\n\n')}] %}
-                {%- endif %}
-                {%- set merged_content = ns_c.chunks %}
-            {%- else %}
-                {%- set merged_content = ns_c.text_parts | join('\n\n') %}
-            {%- endif %}
-            {%- if ns_c.tool_calls | length > 0 %}
-                {%- set ns_agg.messages = ns_agg.messages + [{'role': ns_agg.current_role, 'content': merged_content, 'tool_calls': ns_c.tool_calls}] %}
-            {%- else %}
-                {%- set ns_agg.messages = ns_agg.messages + [{'role': ns_agg.current_role, 'content': merged_content}] %}
-            {%- endif %}
-        {%- endif %}
-        {%- if message['role'] != '__sentinel__' %}
-            {%- set ns_agg.current_group = [message] %}
-            {%- set ns_agg.current_role = message['role'] %}
-        {%- endif %}
-    {%- else %}
-        {%- set ns_agg.current_group = ns_agg.current_group + [message] %}
-    {%- endif %}
-{%- endfor %}
-{%- set loop_messages = ns_agg.messages %}
-
-{#- Validates message ordering. #}
-{%- set ns = namespace(available_tools_and_settings_emitted=false) %}
-{%- if loop_messages | length > 0 and loop_messages[0]['role'] not in ['user', 'system'] %}
-    {{- raise_exception('Conversation must start with a user or system message, got ' + loop_messages[0]['role'] + '.') }}
-{%- endif %}
-{%- set ns_order = namespace(previous_role=none) %}
-{%- for message in loop_messages %}
-    {%- set current_role = message['role'] %}
-    {%- if ns_order.previous_role is not none %}
-        {%- if ns_order.previous_role == 'system' %}
-            {%- if current_role not in ['user', 'assistant', 'system'] %}
-                {{- raise_exception('Unexpected role \'' + current_role + '\' after role \'' + ns_order.previous_role + '\'') }}
-            {%- endif %}
-        {%- elif ns_order.previous_role == 'user' %}
-            {%- if current_role not in ['assistant', 'system', 'user'] %}
-                {{- raise_exception('Unexpected role \'' + current_role + '\' after role \'' + ns_order.previous_role + '\'') }}
-            {%- endif %}
-        {%- elif ns_order.previous_role == 'assistant' %}
-            {%- if current_role not in ['assistant', 'user', 'tool'] %}
-                {{- raise_exception('Unexpected role \'' + current_role + '\' after role \'' + ns_order.previous_role + '\'') }}
-            {%- endif %}
-        {%- elif ns_order.previous_role == 'tool' %}
-            {%- if current_role not in ['assistant', 'tool', 'user'] %}
-                {{- raise_exception('Unexpected role \'' + current_role + '\' after role \'' + ns_order.previous_role + '\'') }}
-            {%- endif %}
-        {%- endif %}
-    {%- endif %}
-    {%- set ns_order.previous_role = current_role %}
-{%- endfor %}
-
-{#- Handle conversation messages. #}
-{%- for message in loop_messages %}
-    {#- User messages supports text, image and image_url content. #}
-    {%- if message['role'] == 'user' %}
-        {%- if not ns.available_tools_and_settings_emitted %}
-            {{- available_tools }}
-            {{- model_settings }}
-            {%- set ns.available_tools_and_settings_emitted = true %}
-        {%- endif %}
-        {%- if message['content'] is not string and message['content'] %}
-            {#- When content has exactly one image and one text block, put image first. #}
-            {%- if message['content'] | length == 2 and message['content'][0]['type'] == 'text' and message['content'][1]['type'] in ['image', 'image_url'] %}
-                {%- set blocks = [message['content'][1], message['content'][0]] %}
-            {%- else %}
-                {%- set blocks = message['content'] %}
-            {%- endif %}
-            {%- set user_content = blocks %}
-        {%- else %}
-            {%- set user_content = message['content'] %}
-        {%- endif %}
-        {{- '[INST]' -}}
-        {{- render_content(user_content, 'user message content', supported_types_desc='text, image and image_url', support_thinking=false, support_images=true) -}}
-        {{- '[/INST]' }}
-
-    {#- Assistant messages supports text and thinking content. #}
-    {%- elif message['role'] == 'assistant' %}
-        {%- if (message['content'] is none or message['content'] == '' or message['content']|length == 0) and (message['tool_calls'] is not defined or message['tool_calls'] is none or message['tool_calls']|length == 0) %}
-            {{- raise_exception('Assistant message must have a string or a list of chunks in content or a list of tool calls.') }}
-        {%- endif %}
-
-        {%- if message['content'] %}
-            {{- render_content(message['content'], 'assistant message contents', supported_types_desc='text and thinking', support_thinking=true, support_images=false) -}}
-        {%- endif %}
-
-        {%- if message['tool_calls'] is defined and message['tool_calls'] is not none and message['tool_calls']|length > 0 %}
-            {%- for tool in message['tool_calls'] %}
-                {{- '[TOOL_CALLS]' }}
-                {%- set name = tool['function']['name'] %}
-                {%- set arguments = tool['function']['arguments'] %}
-                {%- if arguments is not string %}
-                    {%- set arguments = arguments|tojson|safe %}
-                {%- elif arguments == '' %}
-                    {%- set arguments = '{}' %}
-                {%- endif %}
-                {{- name + '[ARGS]' + arguments }}
-            {%- endfor %}
-        {%- endif %}
-
-        {{- eos_token }}
-
-    {#- Tool messages (multimodal). #}
-    {%- elif message['role'] == 'tool' %}
-        {{- '[TOOL_RESULTS]' -}}
-        {{- render_content(message['content'], 'tool message contents', supported_types_desc='text and image', support_images=true) -}}
-        {{- '[/TOOL_RESULTS]' }}
-
-    {#- System messages. #}
-    {%- elif message['role'] == 'system' %}
-        {{- '[SYSTEM_PROMPT]' -}}
-        {{- render_content(message['content'], 'system message contents', supported_types_desc='text', support_thinking=false, support_images=false) -}}
-        {{- '[/SYSTEM_PROMPT]' -}}
-
-    {#- Raise exception for unsupported roles. #}
-    {%- else %}
-        {{- raise_exception('Only user, assistant, system and tool roles are supported, got ' + message['role'] + '.') }}
-    {%- endif %}
-{%- endfor %}